Axiom Math has published a complete formalisation in the Lean proof language of the classification of finite simple groups, one of the largest theorems in mathematics. The project follows the first-generation proof, which is spread across hundreds of papers, and runs to 43.1 million lines of Lean with 2.05 million declarations. Every logical step was checked by the Lean kernel. The team says it found and fixed 34 deviations from published arguments, including a problem in the so-called Unbalanced Group Theorem.

What it means: The news matters beyond pure mathematics because it shows that machine-checked correctness can now be applied at the scale of tens of millions of lines. Until recently, formal verification was seen as too expensive for anything beyond small, critical pieces of software. Combining tools such as Lean with AI models that write and repair proofs is cutting that cost quickly. The fact that the team found dozens of places where published arguments were not exact, even though the theorem stands, is a reminder that work reviewed by experts for decades still has gaps, just like code that has passed many reviews. For finance and payment infrastructure, the trend has a practical side: interest calculation rules, tax logic or smart contracts could be proven correct mathematically rather than only tested. Greek development teams do not need to change tools right away, but it is worth following AI-assisted verification tools and considering a pilot on small, critical parts of code, such as VAT calculations or payment approval rules.

Read the original on Axiom Math

Related service: Custom software

Related stories