Related papers: An Alternative Approach to Formal Mathematics that…
In order to work with mathematical content in computer systems, it is necessary to represent it in formal languages. Ideally, these are supported by tools that verify the correctness of the content, allow computing with it, and produce…
Real-life conjectures do not come with instructions saying whether they they should be proven or, instead, refuted. Yet, as we now know, in either case the final argument produced had better be not just convincing but actually verifiable in…
Informal logic is a method of argument analysis which is complementary to that of formal logic, providing for the pragmatic treatment of features of argumentation which cannot be reduced to logical form. The central claim of this paper is…
Formal logic has often been seen as uniquely placed to analyze mathematical argumentation. While formal logic is certainly necessary for a complete understanding of mathematical practice, it is not sufficient. Important aspects of…
Interactive proof assistants make it possible for ordinary mathematicians to write definitions and theorems in a formal proof language, like a programming language, so that a computer can parse them and check them against the rules of a…
Artificial intelligence assisted mathematical proof has become a highly focused area nowadays. One key problem in this field is to generate formal mathematical proofs from natural language proofs. Due to historical reasons, the formal proof…
Despite significant advancements in the conception of (formal) integrated development environments, applying formal methods in software industry is still perceived as a difficult task. To make the task easier, providing tools that help…
Mathematics formalisation is the task of writing mathematics (i.e., definitions, theorem statements, proofs) in natural language, as found in books and papers, into a formal language that can then be checked for correctness by a program. It…
Alonzo is a practice-oriented classical higher-order version of predicate logic that extends first-order logic and that admits undefined expressions. Named in honor of Alonzo Church, Alonzo is based on Church's type theory, Church's…
This paper describes the design and implementation of mechanisms for light-weight inclusion of formal mathematics in informal mathematical writings, particularly in a Web-based setting. This is conceptually done in three stages: (i) by…
Verifying mathematical proofs is difficult, but can be automated with the assistance of a computer. Autoformalization is the task of automatically translating natural language mathematics into a formal language that can be verified by a…
In AI-rich higher education, polished written mathematics has become easier to produce than trustworthy evidence of understanding. This article develops a human-scale methodology for service mathematics, with informatics as its main running…
Education in the practical applications of logic and proving such as the formal specification and verification of computer programs is substantially hampered by the fact that most time and effort that is invested in proving is actually…
This essay considers the special character of mathematical reasoning, and draws on observations from interactive theorem proving and the history of mathematics to clarify the nature of formal and informal mathematical language. It proposes…
The persisting gap between the formal and the informal mathematics is due to an inadequate notion of mathematical theory behind the current formalization techniques. I mean the (informal) notion of axiomatic theory according to which a…
Mathematical proofs are often said to justify their conclusions by indicating the existence of a corresponding formal derivation. We argue that this widespread view relies on an under-examined notion of correspondence, or what it means for…
AI for Mathematics (AI4Math) is not only intriguing intellectually but also crucial for AI-driven discovery in science, engineering, and beyond. Extensive efforts on AI4Math have mirrored techniques in NLP, in particular, training large…
Since the early twentieth century, it has been understood that mathematical definitions and proofs can be represented in formal systems systems with precise grammars and rules of use. Building on such foundations, computational proof…
For many decades, formal methods are considered to be the way forward to help the software industry to make more reliable and trustworthy software. However, despite this strong belief and many individual success stories, no real change in…
The sequent calculus is a formalism for proving validity of statements formulated in First-Order Logic. It is routinely used in computer science modules on mathematical logic. Formal proofs in the sequent calculus are finite trees obtained…