Prove-It: A Proof Assistant for Organizing and Verifying General Mathematical Knowledge

• URL: http://arxiv.org/abs/2012.10987v2
• Date: Sat, 26 Dec 2020 16:38:05 GMT
• Title: Prove-It: A Proof Assistant for Organizing and Verifying General Mathematical Knowledge
• Authors: Wayne M. Witzel, Warren D. Craft, Robert D. Carr and Joaqu\'in E. Madrid Larra\~naga
• Abstract summary: We introduce Prove-It, a Python-based general-purpose interactive theorem-proving assistant. Prove-It uses a highly-flexible Jupyter notebook-based user interface that documents interactions and proof steps. Current development and future work includes promising applications to quantum circuit manipulation and quantum algorithm verification.
• Score: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: We introduce Prove-It, a Python-based general-purpose interactive theorem-proving assistant designed with the goal of making formal theorem proving as easy and natural as informal theorem proving (with moderate training). Prove-It uses a highly-flexible Jupyter notebook-based user interface that documents interactions and proof steps using LaTeX. We review Prove-It's highly expressive representation of expressions, judgments, theorems, and proofs; demonstrate the system by constructing a traditional proof-by-contradiction that $\sqrt{2}\notin\mathbb{Q}$; and discuss how the system avoids inconsistencies such as Russell's and Curry's paradoxes. Extensive documentation is provided in the appendices about core elements of the system. Current development and future work includes promising applications to quantum circuit manipulation and quantum algorithm verification.

Related papers

• Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
  We present Lean-STaR, a framework for training language models to produce informal thoughts prior to each step of a proof. Lean-STaR achieves state-of-the-art results on the miniF2F-test benchmark within the Lean theorem proving environment.
  arXiv  Detail & Related papers  (2024-07-14T01:43:07Z)
• Proving Theorems Recursively [80.42431358105482]
  We propose POETRY, which proves theorems in a level-by-level manner. Unlike previous step-by-step methods, POETRY searches for a sketch of the proof at each level. We observe a substantial increase in the maximum proof length found by POETRY, from 10 to 26.
  arXiv  Detail & Related papers  (2024-05-23T10:35:08Z)
• Automated Completion of Statements and Proofs in Synthetic Geometry: an Approach based on Constraint Solving [0.0]
  We propose a framework for completing incomplete conjectures and incomplete proofs. The framework can turn a conjecture with missing assumptions into a proper theorem. Also, the proposed framework can help in completing a proof sketch into a human-readable and machine-checkable proof.
  arXiv  Detail & Related papers  (2024-01-22T12:49:08Z)
• Verifying Quantum Phase Estimation (QPE) using Prove-It [0.0]
  The general-purpose interactive theorem-proving assistant called Prove-It was used to verify the Quantum Phase Estimation (QPE) algorithm. Prove-It is unique in its ability to express sophisticated mathematical statements, including statements about quantum circuits.
  arXiv  Detail & Related papers  (2023-04-05T01:21:00Z)
• ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics [7.607254619341369]
  We introduce ProofNet, a benchmark for autoformalization and formal proving of undergraduate-level mathematics. The ProofNet benchmarks consists of 371 examples, each consisting of a formal theorem statement in Lean 3. We report baseline results on statement autoformalization via in-context learning.
  arXiv  Detail & Related papers  (2023-02-24T03:28:46Z)
• Towards Autoformalization of Mathematics and Code Correctness: Experiments with Elementary Proofs [5.045988012508899]
  Autoformalization seeks to address this by translating proofs written in natural language into a formal representation that is computer-verifiable via interactive theorem provers. We introduce a semantic parsing approach, based on the Universal Transformer architecture, that translates elementary mathematical proofs into an equivalent formalization in the language of the Coq interactive theorem prover.
  arXiv  Detail & Related papers  (2023-01-05T17:56:00Z)
• NaturalProver: Grounded Mathematical Proof Generation with Language Models [84.2064569475095]
  Theorem proving in natural mathematical language plays a central role in mathematical advances and education. We develop NaturalProver, a language model that generates proofs by conditioning on background references. NaturalProver is capable of proving some theorems that require short (2-6 step) proofs, and providing next-step suggestions that are rated as correct and useful over 40% of the time.
  arXiv  Detail & Related papers  (2022-05-25T17:01:18Z)
• Generating Natural Language Proofs with Verifier-Guided Search [74.9614610172561]
  We present a novel stepwise method NLProofS (Natural Language Proof Search) NLProofS learns to generate relevant steps conditioning on the hypothesis. It achieves state-of-the-art performance on EntailmentBank and RuleTaker.
  arXiv  Detail & Related papers  (2022-05-25T02:22:30Z)
• Generative Language Modeling for Automated Theorem Proving [94.01137612934842]
  This work is motivated by the possibility that a major limitation of automated theorem provers compared to humans might be addressable via generation from language models. We present an automated prover and proof assistant, GPT-f, for the Metamath formalization language, and analyze its performance.
  arXiv  Detail & Related papers  (2020-09-07T19:50:10Z)
• Learning to Prove Theorems by Learning to Generate Theorems [71.46963489866596]
  We learn a neural generator that automatically synthesizes theorems and proofs for the purpose of training a theorem prover. Experiments on real-world tasks demonstrate that synthetic data from our approach improves the theorem prover.
  arXiv  Detail & Related papers  (2020-02-17T16:06:02Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.