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.