An official website of the United States government
We present PUTNAMBENCH, a new multilingual benchmark for evaluating the ability of neural theorem-provers to solve competition mathematics problems. PUTNAMBENCH consists of 1697 hand-constructed formalizations of 640 theorems sourced from the William Lowell Putnam Mathematical Competition, the premier undergraduate-level mathematics competition in North America. All the theorems have formalizations in Lean 4 and Isabelle; a substantial subset also has Coq formalizations. Proving the theorems requires significant problem-solving ability and proficiency in a broad range of topics taught in undergraduate mathematics courses. We use PUTNAMBENCH to evaluate several established neural and symbolic theorem-provers. These approaches can only solve a handful of the PUTNAMBENCH problems, establishing the benchmark as a difficult open challenge for research on neural theorem-proving. PUTNAMBENCH is available at https://github.com/trishullab/PutnamBench.
more »
« less
Formalizing chemical physics using the Lean theorem prover
Interactive theorem provers are computer programs that check whether mathematical statements are correct. We show how the mathematics of theories in chemical physics can be written in the language of the Lean theorem prover, allowing chemical theory to be made even more rigorous and providing insight into the mathematics behind a theory. We use Lean to precisely define the assumptions and derivations of the Langmuir and BET theories of adsorption. We can also go further and create a network of definitions that build off of each other. This allows us to define a common basis for equations of motion or thermodynamics and derive many statements about them, like the kinematic equations of motion or gas laws such as Boyle's law. This approach could be extended beyond chemistry, and we propose the creation of a library of formally-proven theories in all fields of science. Furthermore, the rigorous logic of theorem provers complements the generative capabilities of AI models that generate code; we anticipate their integration to be valuable for automating the discovery of new scientific theories.
more »
« less
- PAR ID:
- 10488560
- Publisher / Repository:
- Digital Discovery
- Date Published:
- Journal Name:
- Digital Discovery
- ISSN:
- 2635-098X
- Format(s):
- Medium: X
- Sponsoring Org:
- National Science Foundation
More Like this
-
-
We present PutnamBench, a new multi-language benchmark for evaluating the ability of neural theorem-provers to solve competition mathematics problems. PutnamBench consists of 1692 hand-constructed formalizations of 640 theorems sourced from the William Lowell Putnam Mathematical Competition, the premier undergraduate-level mathematics competition in North America. All the problems have formalizations in Lean 4 and Isabelle; a substantial subset also has Coq formalizations. PutnamBench requires significant problem-solving ability and proficiency in a broad range of topics taught in undergraduate mathematics courses. We use PutnamBench to evaluate several established neural and symbolic theorem-provers. These approaches can only solve a handful of the PutnamBench problems, establishing the benchmark as a difficult open challenge for research on neural theorem-proving. PutnamBench is available at https://github.com/trishullab/PutnamBench.more » « less
-
Cook, S.; Katz, B.; Moore-Russo D. (Ed.)Learning to interpret proofs is an important milepost in the maturity and development of students of higher mathematics. A key learning objective in proof-based courses is to discern whether a given proof is a valid justification of its underlying claim. In this study, we presented students with conditional statements and associated proofs and asked them to determine whether the proofs proved the statements and to explain their reasoning. Prior studies have found that inexperienced provers often accept the proof of a statement’s converse and reject proofs by contraposition, which are both erroneous determinations. Our study contributes to the literature by corroborating these findings and suggesting a connection between students’ reading comprehension and proof validation behaviors and their beliefs about mathematical proof and mathematical knowledge base.more » « less
-
Despite their successes, machine learning techniques are often stochastic, error-prone and blackbox. How could they then be used in fields such as theoretical physics and pure mathematics for which error-free results and deep understanding are a must? In this Perspective, we discuss techniques for obtaining zero-error results with machine learning, with a focus on theoretical physics and pure mathematics. Non-rigorous methods can enable rigorous results via conjecture generation or verification by reinforcement learning. We survey applications of these techniques-for-rigor ranging from string theory to the smooth 4D Poincaré conjecture in low-dimensional topology. We also discuss connections between machine learning theory and mathematics or theoretical physics such as a new approach to field theory motivated by neural network theory, and a theory of Riemannian metric flows induced by neural network gradient descent, which encompasses Perelman’s formulation of the Ricci flow that was used to solve the 3D Poincaré conjecture.more » « less
-
The weak gravity conjecture holds that in a theory of quantum gravity any gauge force must mediate interactions stronger than gravity for some particles. This statement has surprisingly deep and extensive connections to many different areas of physics and mathematics. Several variations on the basic conjecture have been proposed, including statements that are much stronger but are nonetheless satisfied by all known consistent quantum gravity theories. These related conjectures and the evidence for their validity in the string theory landscape are reviewed. Also reviewed are a variety of arguments for these conjectures, which tend to fall into two categories: qualitative arguments that claim the conjecture is plausible based on general principles and quantitative arguments for various special cases or analogs of the conjecture. The implications of these conjectures for particle physics, cosmology, general relativity, and mathematics are also outlined. Finally, important directions for future research are highlighted.more » « less
- Free Publicly Accessible Full Text
-
Accepted Manuscript1.0
- Journal Article:
- https://doi.org/10.1039/D3DD00077J
