/Evariste

HyperTree Proof Search for Neural Theorem Proving -- "La science est l'œuvre de l'esprit humain, qui est plutôt destiné à étudier qu'à connaître, à chercher qu'à trouver la vérité."

Primary LanguagePythonOtherNOASSERTION

Evariste

Code accompanying the research paper HyperTree Proof Search for Neural Theorem Proving.

For archival purposes -- this code does NOT run out of the box as we removed references to Meta-internal systems without fixing up entry points for generic setups.

Please view this code as an artifact accompanying the research paper with additional implementation details and as inspiration for future theorem proving systems. We do welcome PRs however that aim to make this repository more accessible.

Contact:

Copyright

The majority of Evariste is licensed under CC-BY-NC, however portions of the project are available under separate license terms: lean_fork (including leanml), lean_proof_recoding and Lean Gym are licensed Apache 2.0.

Citation

Lample, Guillaume, Timothee Lacroix, Marie-Anne Lachaux, Aurelien Rodriguez, Amaury Hayat, Thibaut Lavril, Gabriel Ebner, and Xavier Martinet. "Hypertree proof search for neural theorem proving." Advances in neural information processing systems 35 (2022): 26337-26349.