#Language proof and logic world 3.15 how to
#Language proof and logic world 3.15 verification

In these machine-oriented methods, the original statement of the proposition to be proved is first reduced to a normal form and mechanically manipulated with a small set of inference rules.

Requiring a human-like approach to reasoning means that many automated reasoning methods such as SMT-solvers and resolution (see Section 2.6) must be ruled out. Making a prover which mimics a human's thought process also helps overcome the problem of differing attitudes of correctness. One way in which to improve this situation is to reduce the cost of learning to use proof assistants through making the way in which they process proofs more similar to how a human would process proofs, making the proofs more closely match what the mathematician already knows. Section 1.1 presented three problems that mathematicians have with theorem provers: differing attitudes on correctness, a high learning cost to learning to use ITP and a low resulting reward - learning the truth of something that they 'knew' was true anyway. In Section 1.1, I noted that non-specialist mathematicians have yet to widely accept proof assistants despite the adoption of other tools such as computer algebra systems. I use these improvements to motivate the design choices of the HumanProof system. Motivationīuilding on the background where I explored the literature on the definition of 'human-like' ( Section 2.6) and 'understandable' ( Section 2.5.1) proofs, my goal in this section is find some specific improvements to the way in which computer aided mathematics is done. Then, I will detail the natural language generation pipeline for HumanProof in Section 3.6. This theoretical basis will then be used to define the human-like tactics in Section 3.5.

#Language proof and logic world 3.15 how to

The theory behind creating valid proof terms from Boxes is presented in Section 3.4 as well as how to run standard tactics within Boxes ( Section 3.4.4). In Section 3.3 I provide the details and theory of how the system works through defining the key Box structure and tactics on Boxes. Then in Section 3.2 I give an overview of the resulting designs and underline the primary design decisions and the evidence that drives them. In Section 3.1, I first present an example proof produced by a human to highlight the key features of 'human-like' reasoning that I wish to emulate. Later, in Chapter 6, I gather thoughts and ratings from real mathematicians about the extent to which the developed system achieves these goals. In this chapter I investigate some ways in which the inference rules that provers use could be made more human-like, and then introduce a new proving abstraction layer, HumanProof, written in the Lean 3 theorem prover, implementing these ideas. However, I argue that there are certain ways in which the current methods for performing ITP should be closer to the general cluster of ways in which humans talk about and solve problems. Humans think differently to each other, and I do not wish to state that there is a 'right' way to perform mathematics.

I provided a review to answer this question in Section 2.6. The first research question of Section 1.2 was to investigate what it means for a proof to be human-like.

#Language proof and logic world 3.15 verification

Using an existing prover also means that the verification of proofs can be outsourced to the prover's kernel. HumanProof integrates with an existing proof assistant (in this case Lean).īy plugging in to an existing prover, it is possible to gain leverage by utilising the already developed infrastructure for that prover such as parsers, tactics and automation. This enables compatibility between Box-style proofs and existing automation and verification within Lean.

In the supplementary Appendix A, an 'escape hatch' from the Box datastructure to a metavariable-oriented goal state system as used by Lean ( Section 3.4.4, Appendix A). The Box datastructure, a development calculus ( Section 3.3) designed to better capture how humans reason about proofs while also being formally sound.Ī set of inference rules on Box which preserve this soundness ( Section 3.5).Ī natural language write-up component converting proof objects created with this layer to an interactive piece of text ( Section 3.6).

The driving principle is to find ways of representing proofs at the same level of detail that a human mathematician would use to communicate to colleagues. Now that we have reviewed the requisite background material, I can define the moving parts of a human-like theorem prover. Previously published work and collaboration