google-deepmind/formal-conjectures

A collection of formalised statements of conjectures in Lean, using mathlib. Explore the docs: Formal Conjectures Documentation Join our channel on the leanprover Zulip While there is a growing corpus of formalised theorems including proofs, there is a lack of open conjectures where only the statement has been formalised. This would be useful for a few reasons. It could Become a great benchmark for automated theorem provers and automated formalisation tools. Help clarify the precise meaning of conjectures through formalisation. Encourage the expansion of mathlib by highlighting needed definiti…