lean
Everything on Ground Truth tagged “lean” — 2 items.
The non-sofic group is the one OpenAI claim a computer can check News
Chapter 3 of OpenAI's new manuscript claims to have constructed a non-sofic group, settling a long-open question, and ships roughly 34,000 lines of Lean code with no unproved placeholders so outsiders can verify it.
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.