Learning Formal Mathematics From Intrinsic Motivation — part 4/5
Cleaned-text code points [47517, 63462). Bibliography omitted here; source.md includes it.
t_example1. [(’x : nat) -> (’y : nat) -> (’z : nat) -> (= (+ (* x y) z) (+ (* x y) z))] t_example2. [(’x : nat) -> (’y : nat) -> (= ’y (+ ’x n7)) -> (= (* n2 ’y) (* n2 (+ ’x n7)))] t_example3. [(’a : nat) -> (’b : nat) -> (= (s ’a) ’b) -> (= (s (s ’a)) (s ’b))] t_add_succ_zero. [(’a : nat) -> (= (+ ’a (s z)) (s ’a))] a_zero_add. [(’n : nat) -> (= (+ z ’n) ’n)] a_add_assoc. [(’a : nat) -> (’b : nat) -> (’c : nat) -> (= (+ (+ ’a ’b) ’c) (+ ’a (+ ’b ’c)))] a_succ_add. [(’a : nat) -> (’b : nat) -> (= (+ (s ’a) ’b) (s (+ ’a ’b)))] a_succ_eq_add_one. [(’n : nat) -> (= (s ’n) (+ ’n (s z)))] m_zero_mul. [(’m : nat) -> (= (* z ’m) z)] m_mul_one. [(’m : nat) -> (= (* ’m (s z)) ’m)]
Notably, we give below the full proof our best agent for Arithmetic finds for a_succ_add :
theorem a_succ_add : [(’a0 : nat) -> (’a1 : nat) -> (= (+ (s ’a0) ’a1) (s (+ ’a0 ’a1)))] { intro x : nat. apply nat_ind. goal (= (+ (s x) z) (s (+ x z))) { show (= (+ (s x) z) (s x)) by +_z. show (= (+ x z) x) by +_z. show (= x (+ x z)) by eq_symm. show (= (+ (s x) z) (s (+ x z))) by rewrite. } goal [(’n : nat) -> (= (+ (s x) ’n) (s (+ x ’n))) -> (= (+ (s x) (s ’n)) (s (+ x (s ’n))))] { intro x0 : nat. intro x1 : (= (+ (s x) x0) (s (+ x x0))). show (= (s (+ x x0)) (+ (s x) x0)) by eq_symm. show (= (+ (s x) x0) (+ (s x) x0)) by rewrite. show (= (s (+ x x0)) (s (+ x x0))) by rewrite. show (= (+ x (s x0)) (s (+ x x0))) by +_s. show (= (+ x (s x0)) (+ (s x) x0)) by rewrite. show (= (s (+ x x0)) (+ x (s x0))) by eq_symm. show (= (+ (s x) x0) (+ x (s x0))) by rewrite. show (= (+ x (s x0)) (+ x (s x0))) by rewrite. show (= (+ (s x) (s x0)) (s (+ (s x) x0))) by +_s. show (= (+ (s x) (s x0)) (s (+ x (s x0)))) by rewrite. } }
This proof is not minimal – our human-written Peano proof for this level of the game has 7 steps in the inductive case, compared to 12 in the proof the agent finds. Nevertheless, this is a non-trivial theorem to prove by hand in this low-level axiomatic system, and our agent was not explicitly trained to target this theorem. Thus, this shows that it does learn general patterns that are useful in proof search.
### E.2 Propositional Logic
We here list all the statements in Theorem 41 of Kleene’s book [ 20 ] , “Introduction to Metamathematics”, represented in Peano:
1. [(’A : prop) -> [’A -> ’A]] 2. [(’A : prop) -> (’B : prop) -> (’C : prop) -> [’A -> ’B] -> [’B -> ’C] -> [’A -> ’C]] 3. [(’A : prop) -> (’B : prop) -> (’C : prop) -> [’A -> [’B -> ’C]] -> [’B -> [’A -> ’C]]] 4. [(’A : prop) -> (’B : prop) -> (’C : prop) -> [’A -> [’B -> ’C]] -> [(and ’A ’B) -> ’C]] 5. [(’A : prop) -> (’B : prop) -> (’C : prop) -> [(and ’A ’B) -> ’C] -> [’A -> [’B -> ’C]]] 6. [(’A : prop) -> (’B : prop) -> (’C : prop) -> [’A -> ’B] -> [[’B -> ’C] -> [’A -> ’C]]] 7. [(’A : prop) -> (’B : prop) -> (’C : prop) -> [’A -> ’B] -> [[’C -> ’A] -> [’C -> ’B]]] 8a. [(’A : prop) -> (’B : prop) -> (’C : prop) -> [’A -> ’B] -> [(and ’A ’C) -> (and ’B ’C)]] 8b. [(’A : prop) -> (’B : prop) -> (’C : prop) -> [’A -> ’B] -> [(and ’C ’A) -> (and ’C ’B)]] 9a. [(’A : prop) -> (’B : prop) -> (’C : prop) -> [’A -> ’B] -> [(or ’A ’C) -> (or ’B ’C)]] 9b. [(’A : prop) -> (’B : prop) -> (’C : prop) -> [’A -> ’B] -> [(or ’A ’C) -> (or ’B ’C)]] 10a. [(’A : prop) -> (’B : prop) -> [(not ’A) -> [’A -> ’B]]] 10b. [(’A : prop) -> (’B : prop) -> [’A -> [(not ’A) -> ’B]]] 11. [(’A : prop) -> (’B : prop) -> [’B -> [’A -> ’B]]] 12. [(’A : prop) -> (’B : prop) -> [’A -> ’B] -> [(not ’B) -> (not ’A)]] 13. [(’A : prop) -> (’B : prop) -> [’A -> (not ’B)] -> [’B -> (not ’A)]] 14. [(’A : prop) -> (’B : prop) -> [(not ’A) -> ’B] -> [(not ’B) -> ’A]] 15. [(’A : prop) -> (’B : prop) -> [(not ’A) -> (not ’B)] -> [’B -> ’A]] 16. [(’A : prop) -> (’B : prop) -> [’A -> ’B] -> [’B -> ’A] -> (iff ’A ’B)] 17a. [(’A : prop) -> (’B : prop) -> (iff ’A ’B) -> [’A -> ’B]] 17b. [(’A : prop) -> (’B : prop) -> (iff ’A ’B) -> [’B -> ’A]] 18a. [(’A : prop) -> (’B : prop) -> (iff ’A ’B) -> ’A -> ’B] 18b. [(’A : prop) -> (’B : prop) -> (iff ’A ’B) -> ’B -> ’A] 19. [(’A : prop) -> (iff ’A ’A)] 20. [(’A : prop) -> (’B : prop) -> (iff ’A ’B) -> (iff ’B ’A)] 21. [(’A : prop) -> (’B : prop) -> (’C : prop) -> (iff ’A ’B) -> (iff ’B ’C) -> (iff ’A ’C)] 22. [(’A : prop) -> (’B : prop) -> (’C : prop) -> [’A -> [’B -> ’C]] -> [(not (not ’A)) -> [(not (not ’B)) -> (not (not ’C))]]] 23. [(’A : prop) -> (’B : prop) -> [(not (not [’A -> ’B]))] -> [(not (not ’A)) -> (not (not ’B))]] 24. [(’A : prop) -> (’B : prop) -> (’C : prop) -> [(not (not [’A -> ’B]))] -> [(not (not [’B -> ’C]))] -> [(not (not [’A -> ’C]))]] 25. [(’A : prop) -> (’B : prop) -> (iff (not (not (and ’A ’B))) (and (not (not ’A)) (not (not ’B))))]
We use the numbering from the book here — there are 30 statements, even if the last one is labeled 25.
## Appendix F Discussion: extension to other proof assistants
While our approach is implemented in Peano, it can in principle be extended to mainstream theorem provers like Lean and Coq. Peano’s typing rules (a version of the Calculus of Constructions, without native inductive types) are essentially a subset of these systems’ more expressive calculi, and its minimalism makes it particularly suitable for automated proof search. The most practical path to integration would be similar to recent tools like Duper [ 9 ] : embedding problems from the target system (e.g., Lean) into a Peano representation, running the prover, and then reconstructing the discovered proofs in the original system. While developing a Peano-to-Lean proof object translator would be relatively straightforward given the simplicity of Peano’s type system, translating arbitrary Lean problems to Peano would require significant more engineering effort (e.g., we would need to generate explicit axioms for inductive types and quotients, which are not part of Peano). However, we believe a simplified environment is valuable for investigating how self-improving agents can build towards deeper theorems, eventually being able to invent new definitions and accumulate a growing library (which Minimo does not, yet). Once these capabilities are demonstrated convincingly, the engineering investment in proof translation will become more compelling.
## NeurIPS Paper Checklist
1. Claims
Question: Do the main claims made in the abstract and introduction accurately reflect the paper’s contributions and scope?
Answer: [Yes]
Justification: We claim an approach to training a self-improving mathematical reasoning agent starting just from axioms. This is demonstrated in 3 axiomatic domains in Section 4 .
Guidelines: • The answer NA means that the abstract and introduction do not include the claims made in the paper.
• The abstract and/or introduction should clearly state the claims made, including the contributions made in the paper and important assumptions and limitations. A No or NA answer to this question will not be perceived well by the reviewers.
• The claims made should match theoretical and experimental results, and reflect how much the results can be expected to generalize to other settings.
• It is fine to include aspirational goals as motivation as long as it is clear that these goals are not attained by the paper.
2. Limitations
Question: Does the paper discuss the limitations of the work performed by the authors?
Answer: [Yes]
Justification: Our key limitations are explicitly discussed in Section 5 .
Guidelines: • The answer NA means that the paper has no limitation while the answer No means that the paper has limitations, but those are not discussed in the paper.
• The authors are encouraged to create a separate "Limitations" section in their paper.
• The paper should point out any strong assumptions and how robust the results are to violations of these assumptions (e.g., independence assumptions, noiseless settings, model well-specification, asymptotic approximations only holding locally). The authors should reflect on how these assumptions might be violated in practice and what the implications would be.
• The authors should reflect on the scope of the claims made, e.g., if the approach was only tested on a few datasets or with a few runs. In general, empirical results often depend on implicit assumptions, which should be articulated.
• The authors should reflect on the factors that influence the performance of the approach. For example, a facial recognition algorithm may perform poorly when image resolution is low or images are taken in low lighting. Or a speech-to-text system might not be used reliably to provide closed captions for online lectures because it fails to handle technical jargon.
• The authors should discuss the computational efficiency of the proposed algorithms and how they scale with dataset size.
• If applicable, the authors should discuss possible limitations of their approach to address problems of privacy and fairness.
• While the authors might fear that complete honesty about limitations might be used by reviewers as grounds for rejection, a worse outcome might be that reviewers discover limitations that aren’t acknowledged in the paper. The authors should use their best judgment and recognize that individual actions in favor of transparency play an important role in developing norms that preserve the integrity of the community. Reviewers will be specifically instructed to not penalize honesty concerning limitations.
3. Theory Assumptions and Proofs
Question: For each theoretical result, does the paper provide the full set of assumptions and a complete (and correct) proof?
Answer: [N/A]
Justification: No theoretical results.
Guidelines: • The answer NA means that the paper does not include theoretical results.
• All the theorems, formulas, and proofs in the paper should be numbered and cross-referenced.
• All assumptions should be clearly stated or referenced in the statement of any theorems.
• The proofs can either appear in the main paper or the supplemental material, but if they appear in the supplemental material, the authors are encouraged to provide a short proof sketch to provide intuition.
• Inversely, any informal proof provided in the core of the paper should be complemented by formal proofs provided in appendix or supplemental material.
• Theorems and Lemmas that the proof relies upon should be properly referenced.
4. Experimental Result Reproducibility
Question: Does the paper fully disclose all the information needed to reproduce the main experimental results of the paper to the extent that it affects the main claims and/or conclusions of the paper (regardless of whether the code and data are provided or not)?
Answer: [Yes]
Justification: We list all of the axioms in Peano we use in the Appendix. For conjecturing, we use a public implementation of Synchromesh, together with the completion engine algorithm we describe in Section 3.1 . The MCTS proof search procedure we use is standard, and present in previous papers with open-source implementations [ 42 ] . Nevertheless, we acknowledge that the paper required significant implementation, and thus reproducibility will be much easier with our code release, which we will do after the submission.
Guidelines: • The answer NA means that the paper does not include experiments.
• If the paper includes experiments, a No answer to this question will not be perceived well by the reviewers: Making the paper reproducible is important, regardless of whether the code and data are provided or not.
• If the contribution is a dataset and/or model, the authors should describe the steps taken to make their results reproducible or verifiable.
• Depending on the contribution, reproducibility can be accomplished in various ways. For example, if the contribution is a novel architecture, describing the architecture fully might suffice, or if the contribution is a specific model and empirical evaluation, it may be necessary to either make it possible for others to replicate the model with the same dataset, or provide access to the model. In general. releasing code and data is often one good way to accomplish this, but reproducibility can also be provided via detailed instructions for how to replicate the results, access to a hosted model (e.g., in the case of a large language model), releasing of a model checkpoint, or other means that are appropriate to the research performed.
• While NeurIPS does not require releasing code, the conference does require all submissions to provide some reasonable avenue for reproducibility, which may depend on the nature of the contribution. For example (a) If the contribution is primarily a new algorithm, the paper should make it clear how to reproduce that algorithm.
(b) If the contribution is primarily a new model architecture, the paper should describe the architecture clearly and fully.
(c) If the contribution is a new model (e.g., a large language model), then there should either be a way to access this model for reproducing the results or a way to reproduce the model (e.g., with an open-source dataset or instructions for how to construct the dataset).
(d) We recognize that reproducibility may be tricky in some cases, in which case authors are welcome to describe the particular way they provide for reproducibility. In the case of closed-source models, it may be that access to the model is limited in some way (e.g., to registered users), but it should be possible for other researchers to have some path to reproducing or verifying the results.
5. Open access to data and code
Question: Does the paper provide open access to the data and code, with sufficient instructions to faithfully reproduce the main experimental results, as described in supplemental material?
Answer: [Yes]
Justification: We provide a zip file containing all of our implementation in our supplementary material, and the configuration files and commands used to run the main experiments. This was also released on Github ( https://github.com/gpoesia/minimo ).
Guidelines: • The answer NA means that paper does not include experiments requiring code.
• Please see the NeurIPS code and data submission guidelines ( https://nips.cc/public/guides/CodeSubmissionPolicy ) for more details.
• While we encourage the release of code and data, we understand that this might not be possible, so “No” is an acceptable answer. Papers cannot be rejected simply for not including code, unless this is central to the contribution (e.g., for a new open-source benchmark).
• The instructions should contain the exact command and environment needed to run to reproduce the results. See the NeurIPS code and data submission guidelines ( https://nips.cc/public/guides/CodeSubmissionPolicy ) for more details.
• The authors should provide instructions on data access and preparation, including how to access the raw data, preprocessed data, intermediate data, and generated data, etc.
• The authors should provide scripts to reproduce all experimental results for the new proposed method and baselines. If only a subset of experiments are reproducible, they should state which ones are omitted from the script and why.
• At submission time, to preserve anonymity, the authors should release anonymized versions (if applicable).
• Providing as much information as possible in supplemental material (appended to the paper) is recommended, but including URLs to data and code is permitted.
6. Experimental Setting/Details
Question: Does the paper specify all the training and test details (e.g., data splits, hyperparameters, how they were chosen, type of optimizer, etc.) necessary to understand the results?
Answer: [Yes]
Justification: These are provided in the Appendix, and in the code release.
Guidelines: • The answer NA means that the paper does not include experiments.
• The experimental setting should be presented in the core of the paper to a level of detail that is necessary to appreciate the results and make sense of them.