From 9593f9c5b0365b02d7066371954bf2d983015919 Mon Sep 17 00:00:00 2001
From: Mikhail Nemerov <34755036+deadczarvc@users.noreply.github.com>
Date: Thu, 1 Oct 2026 23:07:05 +0300
Subject: [PATCH 1/2] fix(quality): read an axiom list that Lean wrapped over
 several lines

---
 python/lean_pool/quality.py    |  4 +++-
 python/tests/test_challenge.py | 22 ++++++++++++++++++++++
 2 files changed, 25 insertions(+), 1 deletion(-)

diff --git a/python/lean_pool/quality.py b/python/lean_pool/quality.py
index a99abfda09..b298df3d4a 100644
--- a/python/lean_pool/quality.py
+++ b/python/lean_pool/quality.py
@@ -983,7 +983,9 @@ def _parse_axiom_output(
         {f"_root_.{declaration.name}": declaration for declaration in declarations}
     )
     # Names may contain `'` (e.g. `foo'`); see _axiom_audit_resolved comment.
-    pattern = re.compile(r"^'(.+?)' depends on axioms: \[(.*)\]$", re.MULTILINE)
+    # Past 120 columns Lean wraps the list after each comma, so the list may span
+    # lines: `[^\]]*` crosses newlines, and the split below strips the indents.
+    pattern = re.compile(r"^'(.+?)' depends on axioms: \[([^\]]*)\]", re.MULTILINE)
     seen: set[str] = set()
     for match in pattern.finditer(output):
         name = match.group(1)
diff --git a/python/tests/test_challenge.py b/python/tests/test_challenge.py
index 95ed389ed8..ebb99ce8c2 100644
--- a/python/tests/test_challenge.py
+++ b/python/tests/test_challenge.py
@@ -353,6 +353,28 @@ def test_axiom_audit_allows_sorry_only_for_registered_declarations() -> None:
     assert "Challenge.Widget.helper depends on `sorryAx`" in errors[0].message
 
 
+def test_axiom_audit_reads_a_list_lean_wrapped_over_several_lines() -> None:
+    """Past 120 columns Lean breaks the axiom list after each comma."""
+    declarations = [_declaration("Challenge.TestingByBetting.ville_testing_by_betting")]
+    # Verbatim `#print axioms` output from `lake env lean` (Lean 4.35.0-rc3).
+    output = (
+        "'Challenge.TestingByBetting.ville_testing_by_betting' "
+        "depends on axioms: [propext,\n"
+        " sorryAx,\n"
+        " Classical.choice,\n"
+        " Quot.sound]\n"
+    )
+
+    errors = _parse_axiom_output(
+        Path("/repo"),
+        declarations,
+        output,
+        {"Challenge.TestingByBetting.ville_testing_by_betting"},
+    )
+
+    assert errors == []
+
+
 def test_axiom_audit_requires_registered_statements_to_stay_open() -> None:
     """A statement proved in place is no longer the contract solvers took on."""
     declarations = [_declaration("Challenge.Widget.widget_exists")]

From 36db76fabc7809e1747c3704934062f7cc8c2ee5 Mon Sep 17 00:00:00 2001
From: Mikhail Nemerov <34755036+deadczarvc@users.noreply.github.com>
Date: Fri, 2 Oct 2026 00:05:18 +0300
Subject: [PATCH 2/2] fix(quality): keep the end-of-line anchor; test a wrapped
 unregistered neighbour

---
 python/lean_pool/quality.py    |  3 ++-
 python/tests/test_challenge.py | 24 ++++++++++++++++++++----
 2 files changed, 22 insertions(+), 5 deletions(-)

diff --git a/python/lean_pool/quality.py b/python/lean_pool/quality.py
index b298df3d4a..6bf0cced94 100644
--- a/python/lean_pool/quality.py
+++ b/python/lean_pool/quality.py
@@ -985,7 +985,8 @@ def _parse_axiom_output(
     # Names may contain `'` (e.g. `foo'`); see _axiom_audit_resolved comment.
     # Past 120 columns Lean wraps the list after each comma, so the list may span
     # lines: `[^\]]*` crosses newlines, and the split below strips the indents.
-    pattern = re.compile(r"^'(.+?)' depends on axioms: \[([^\]]*)\]", re.MULTILINE)
+    # `$` still demands that the closing bracket ends its line.
+    pattern = re.compile(r"^'(.+?)' depends on axioms: \[([^\]]*)\]$", re.MULTILINE)
     seen: set[str] = set()
     for match in pattern.finditer(output):
         name = match.group(1)
diff --git a/python/tests/test_challenge.py b/python/tests/test_challenge.py
index ebb99ce8c2..53d5bb4b32 100644
--- a/python/tests/test_challenge.py
+++ b/python/tests/test_challenge.py
@@ -354,15 +354,27 @@ def test_axiom_audit_allows_sorry_only_for_registered_declarations() -> None:
 
 
 def test_axiom_audit_reads_a_list_lean_wrapped_over_several_lines() -> None:
-    """Past 120 columns Lean breaks the axiom list after each comma."""
-    declarations = [_declaration("Challenge.TestingByBetting.ville_testing_by_betting")]
-    # Verbatim `#print axioms` output from `lake env lean` (Lean 4.35.0-rc3).
+    """Past 120 columns Lean breaks the axiom list after each comma.
+
+    Each wrapped list must end at its own bracket: an unregistered neighbour
+    whose wrapped list carries `sorryAx` is still rejected.
+    """
+    declarations = [
+        _declaration("Challenge.TestingByBetting.ville_testing_by_betting"),
+        _declaration("Challenge.TestingByBetting.helper_with_a_long_enough_name"),
+    ]
+    # The first result is verbatim `#print axioms` output from `lake env lean`
+    # (Lean 4.35.0-rc3); the second is wrapped the same way.
     output = (
         "'Challenge.TestingByBetting.ville_testing_by_betting' "
         "depends on axioms: [propext,\n"
         " sorryAx,\n"
         " Classical.choice,\n"
         " Quot.sound]\n"
+        "'Challenge.TestingByBetting.helper_with_a_long_enough_name' "
+        "depends on axioms: [propext,\n"
+        " sorryAx,\n"
+        " Classical.choice]\n"
     )
 
     errors = _parse_axiom_output(
@@ -372,7 +384,11 @@ def test_axiom_audit_reads_a_list_lean_wrapped_over_several_lines() -> None:
         {"Challenge.TestingByBetting.ville_testing_by_betting"},
     )
 
-    assert errors == []
+    assert len(errors) == 1
+    assert (
+        "Challenge.TestingByBetting.helper_with_a_long_enough_name depends on "
+        "`sorryAx`" in errors[0].message
+    )
 
 
 def test_axiom_audit_requires_registered_statements_to_stay_open() -> None: