proof-assistant
Everything on Ground Truth tagged “proof-assistant” — 2 items.
Lean comparator Tool
The Lean toolchain component used to independently check the formalization behind Anthropic's zeta-function result. Useful to anyone who wants machine-verified mathematics rather than a persuasive argument.
Formal Conjectures Tool
Google DeepMind's open Lean library of formally stated open mathematical conjectures, now the venue where the claimed Jacobian conjecture counterexample is being reviewed in public. A usable resource if you want machine-checkable statements of open problems rather than prose.