Aims and Scope

The act of formalizing mathematics 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.

Formalized mathematics is a relatively new field and there are not yet established standards for papers in this discipline. This is a living document, meant to guide both authors and reviewers toward common standards; as the field and the AFM both mature, we expect the criteria and values associated with its papers to change. 

We aim to publish papers across a variety of mathematical disciplines and proof assistant ecosystems. Papers should be written for a mathematical audience and evaluated on their relevance to the field of mathematics. Introductions should be accessible and target a general audience.

We expect papers to be accompanied by formal proof artifacts. In the absence of formal proof artifacts, mathematical insight gained through the application of artificial intelligence tools is not considered within the scope of the AFM.

Proof auditing, the act of checking that formal statements correspond correctly to their informal counterparts, is a difficult and inherently human part of reviewing formalized mathematics. We expect authors to make these correspondences clear, highlighting and explaining potential mismatches, and linking informal statements to formal statements as often as is appropriate.

Virtues of a formalization project

Not every project will excel in all of these criteria, and they are not requirements for a paper to be published in the AFM. Nevertheless we encourage authors and reviewers to take these points into consideration.

• Novelty of the formalization: Has this topic been formalized before? If so, in which proof assistant ecosystems? How does the current formalization relate to existing ones?
• Novelty of the mathematics: Is the subject of the formalization a new or recent result? If so, how significant is the new result? If not, what is the impact and importance of the known result? Is the importance properly discussed in the paper?
• Insightfulness: Did the formalization yield any new mathematical insights? Did it yield any general lessons about how mathematical concepts can or should be represented formally?
• Generality: Does the project take on a specific mathematical topic in detail, or does it work at a high level of abstraction? How widely do the results apply?
• Integration: Does the project build on existing libraries? Has it or will it be integrated into these libraries? How interconnected is it with other parts of the library? Is it incompatible with existing libraries or parts of them?
• Reproducibility: Does this work teach lessons that can be applied in other libraries or proof assistant ecosystems?
• How complex, long, or difficult is the formalization itself?
• Did the choice of proof assistant or logical foundation crucially influence the formalization process?
• How readable and well-documented is the code artifact?

We emphasize a focus on the usability of formalization projects: authors are encouraged to explain the interfaces around their definitions, if applicable with examples of how their development can be used, and to provide all their files with adequate documentation.