Growing Verified Math Knowledge Graph

This turns each solved proof into infrastructure, not just output. Once a fact has been translated into Lean and mechanically checked, it becomes a reusable building block the system can fetch on later problems, much like a programmer importing a tested library instead of rewriting code. In formal math, retrieval matters because many hard proofs depend less on raw creativity than on finding the right prior lemma, definition, or dependency chain inside a large verified library.

• Lean already works this way through Mathlib, a shared library of formal definitions and theorems that users search while proving new results. Axiom is extending that pattern by auto formalizing papers and forum discussions, then feeding verified outputs back into its own store of reusable facts.
  1 leanlang 2 github 4 sacra
• The practical advantage is compounding accuracy. A natural language model may vaguely remember a theorem, but a verified graph can return the exact formal statement and all required prerequisites, which sharply narrows search and reduces hallucinated intermediate steps.
  2 github 3 arxiv 4 sacra
• This also explains why theorem proving products get stronger with use. Harmonic follows a similar path with Lean 4 based verified proofs, but the real moat is not only the model, it is the growing stock of machine checkable results that future proofs can build on immediately.
  5 harmonic 6 sacra

Going forward, the winning systems in formal math will look less like one shot chatbots and more like continuously expanding proof warehouses. As these verified libraries thicken, they can move from solving isolated olympiad style questions to supporting research workflows, quantitative finance, and other domains where reusing trusted mathematical machinery is the whole point.