Axiom Math: Formal proofs need more than correctness

Axiom Math frames AI-generated formal mathematics around three layers: correctness, Lean code quality and mathematical taste. A proof can be formally correct yet still be considered weak because its structure or implementation is sloppy.

For its formalization of the bounded-gap result, completed by Polymath AB, Axiom emphasized reusable Lean code and quality that other communities can build upon. It also argued that human judgment remains important in deciding which theorems matter and may have useful real-world applications.