Aims and Scope

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.

The use of in-text code blocks should be limited to situations in which the code complements the text. We expect reviewers and interested readers to look at code artifacts alongside papers; it is not necessary to reproduce a substantial part of the code artifact in the paper itself. We expect reviewers to run the appropriate software to check code artifacts for correctness.

There are many “virtues” that we look for in 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.