vince-gonzalez/generated-proofs-axioms
What machine-generated Lean proofs rest on Per-theorem axiom dependencies for 9,729 machine-generated Lean 4 proofs. A model writing Lean gets one bit of feedback: the proof compiles, or it does not. What the proof ends up standing on is not part of that signal. This is that measurement, over the Goedel-Prover output for the Lean Workbook problems. Headline Of the 9,169 proofs that still compile under Lean 4.32: count share reach Classical.choice 8,496… See the full description on the dataset page: https://huggingface.co/datasets/vince-gonzalez/generated-proofs-axioms.
Conversations for this repository live on Hugging Face.
CoolFace shows imported repositories read-only. Posting into someone else’s repository from here would need an authorised integration and the account holder’s consent, so the link goes to the source instead.
Open discussions on Hugging Face