What was already known
Sharipov posed the first cuboid irreducibility conjecture in 2011. Valery Asiryan had already given an informal proof of the same result in October 2025 by an elliptic-curve route.
AI involvement
The project attributes discovery of this formal proof route to autonomous AlphaProof Nexus. Codrut Grosu later reconstructed and checked its mathematical argument in full; Asiryan retains priority for the earlier result.
The project explicitly attributes discovery of this distinct formal proof route to an autonomous AlphaProof Nexus run; human publication and later deformalisation are separately credited.
Importance
Provides a distinct formal and elementary proof of the first cuboid irreducibility conjecture.
Limitations
It does not settle Sharipov’s other two irreducibility conjectures or perfect-cuboid existence. The autonomous-run account comes from the project maintainers.
Technical verification
The source reports a sorry-free Lean proof of the exact irreducibility statement with standard axioms. Grosu’s complete deformalisation traces and checks every lemma and tactic in the mathematical argument, documenting both machine and human checking of this proof route. Neither check grants first-result priority over Asiryan.
Formal checking
Sorry-free proof build, standard-axiom audit and exact selected-statement comparison
- Checker
- Lean 4 kernel and Comparator in the reported repository build
- Scope
- Irreducibility of Pₐ,ᵦ for positive coprime unequal integers
- Basis
- Reported by the linked checker
Formal checking
Complete deformalisation tracing every lemma and tactic step and checking logical flow
- Checker
- Codrut Grosu
- Scope
- The formal proof from quartic reduction through descent to final irreducibility
- Basis
- Reported by the linked checker
Checking a formal statement does not establish that it matches the original problem.
Human understanding
Grosu’s complete informal reconstruction and the published proof outline explain the quartic obstruction, infinite-descent mechanism and final factorization argument.
Correction and publication history
Provides a distinct formal and elementary proof of the first cuboid irreducibility conjecture.
Read this published revision