-
-
(x+u)^2=x^2+2xu+u^2
-
(x+u)^2=x^2+2xu+(u^2−G)
-
(x+u+1)^2=x^2+2xu+(u^2+2u+1)
-
(x+u+1+v+w)^2=x^2+u2+1+v^2+w^2+⋯
Inspiration
Mathematical claims can spread faster than they can be independently checked.
A newly reported three-variable candidate counterexample to the Jacobian Conjecture provided a real-time test case: could GPT-5.6, Codex, and Lean turn complicated reported formulas into a precise, reproducible verification package while the broader mathematical review was still beginning?
Breaking Math Verification was built to answer that question.
What it does
The project provides a reusable workflow for transforming an externally reported mathematical claim into:
- an independent Lean reconstruction,
- explicit finite witnesses,
- a selected summit theorem,
- logical consequences,
- a focused axiom audit,
- a provenance record,
- and a stable public Demo surface.
The Jacobian case study formalizes an explicit polynomial map over both the rational and complex numbers.
Lean verifies that the original formal Jacobian determinant is -2. After an exact normalization of the first output coordinate, Lean verifies:
det J(F̃) = 1
Lean then checks three pairwise-distinct inputs:
(0, 0, -1/4)
(1, -3/2, 13/2)
(-1, 3/2, 13/2)
and proves that all three map to the same exact target:
F̃(p₀) = F̃(p₁) = F̃(p₂) = (1/8, 0, 0)
The formalized map is therefore not injective and has no set-theoretic left inverse.
Reusable developer API
The work extracted a small generic Lean API:
DkMath.Verification.CollisionCertificate
DkMath.Verification.CollisionCertificate.notInjective
DkMath.Verification.CollisionCertificate.noLeftInverse
The generic collision consequences are available through the root DkMath import and depend on no axioms.
The project also includes reusable templates for:
- reported claims,
- theorem pipelines,
- provenance,
- scope boundaries,
- Demo contracts,
- and axiom-audit targets.
How GPT-5.6 and Codex were used
GPT-5.6 was used for mathematical decomposition, theorem-boundary design, architecture review, scope control, and checkpoint evaluation.
Codex inspected the live DkMath repository, identified reusable APIs, implemented the Lean modules, ran focused builds and axiom audits, generated structured reports, and built the reproducible video pipeline.
A key engineering decision was to use committed Git repository reports as an auditable handoff channel between GPT-5.6 review and Codex implementation.
The resulting workflow was developed through six checkpoints:
BMV-001 architecture audit
BMV-002 generic collision certificate
BMV-003 Jacobian adapter
BMV-004 verification contracts
BMV-005 cross-domain workflow validation
BMV-006 public DkMath integration
Trust boundary
Lean verifies the exact formulas encoded in the project, the determinant calculations, the explicit collision, and the resulting logical consequences.
It does not certify historical priority, authorship, publication status, peer review, community acceptance, or claims that were not formalized.
The reported candidate remains new and broader mathematical review may continue. Breaking Math Verification supplies a fast, reproducible first verification layer for the exact formulas under discussion.
Demo
Public video:
Repository and testing instructions:
Log in or sign up for Devpost to join the conversation.