Home

Founded in 2024, the Annals of Formalized Mathematics is a MathOA-supported diamond open access overlay journal. It publishes original articles about formalized mathematics and mathematical applications of proof assistants. The journal accepts papers in English that are typically accompanied by a code artifact.

The AFM publishes papers on the mathematical applications of proof assistants and automated reasoning tools. Papers should be written for an audience of mathematicians and should not focus on the details of the tools themselves. Papers do not necessarily need to present novel mathematical proofs but should describe the mathematical lessons learned during the formalization process.

Proof assistants and automated reasoning

Proof assistants, also known as interactive theorem provers, are tools for producing formally correct mathematics. Mathematicians write definitions, theorems, and proofs in a specialized language, with the computer giving instant feedback about each line. Examples of popular proof assistants include Agda, Coq, HOL Light, Isabelle, Lean, and Mizar.

These tools have been used to develop large libraries of "known" mathematics as well as to verify major recent or controversial results. The act of formalizing a proof is not mechanical: it involves substantial mathematical insight in its own right, and it constitutes the essence of formalized mathematics, which is now recognized as a mathematical discipline on its own. Despite its young age, this discipline is blossoming at a very fast pace; it nowadays occupies a significant place in the mathematical horizon.

Related to proof assistants, automated reasoning tools take in the formal statement of a theorem and attempt to prove it without further human input. While the study of these tools themselves is the domain of computer science, their use on mathematical theorems requires sophisticated reductions and reformulations.