Open Source Commoditizes Theorem Proving
Axiom Math
Open source is turning core theorem proving into a fast moving baseline, which means proprietary vendors have to sell a full workflow, not just a stronger model. Lean itself is open source, DeepSeek-Prover-V2 is openly available for Lean 4, and research projects like LeanDojo and Lean Forward keep improving retrieval, proof search, and usability in public. That makes it harder to charge premium prices for basic proof generation alone.
-
The switching cost is low because many projects build on the same Lean 4 stack. A research team can test an open model, plug it into existing Lean tooling, and compare outputs directly, without rewriting its proof environment from scratch.
-
Open projects also improve faster in visible ways. DeepSeek publishes model weights and benchmark results, LeanDojo exposes a reusable environment for training and evaluation, and BFS-Prover-V2 pushes open state of the art on miniF2F and ProofNet. Feature gaps get closed in public, then copied quickly.
-
That shifts commercial value upward into packaging and trust. Axiom’s product chain starts with turning natural language into Lean, then proposing lemmas, proving steps, verifying them, and converting the result back into readable math. Enterprises will pay for that reliable end to end system, not for raw proving alone.
The market is likely to split in two. Open source will keep supplying the base proving engine, while commercial players win by wrapping it in enterprise workflows, domain tuned datasets, support, and compliance grade audit trails. As the base layer gets cheaper and better, pricing power will concentrate in products that save real labor inside regulated research and industrial math teams.