This repository is part of the Formal abstracts projects initiated by Thomas Hales. See his talk Big conjectures from the Big Proof meeting in Cambridge.
A formal abstract, or fabstract for short, is a formalization of the main results (constructions, definitions, proofs, conjectures) of a piece of informal mathematics, such as a research paper. There is no requirement that the entire text be formalized, and you may leave any piece of it unformalized. Commonly, proofs of statements are omitted.
A formal abstract is not the formalization of the abstract itself.
If you are interested in the project, and especially if you plan to contribute, we kindly invite you to join the Formal abstracts mailing list.
Formal abstracts is a collaborative effort. Contributing even a single fabstract, or an improvement of an existing one, is highly appreciated. Do not worry if you do not get it quite right, the curators will help fix it.
You may add your own fabstracts, improve existing ones, and work on the folklore. You may also contribute other people's fabstracts, but please be extra careful to get them right.
Please consult the instructions on how to contribute.
We believe that the fabstracts should be freely available to everyone. Therefore, we use a
permissive Creative Commons license CC-BY-4.0.
If you contribute to the repository, you agree with the license.
This work is licensed under a Creative Commons Attribution 4.0 International License.
The repository was created during the BigProof meeting at Cambridge in July 2017, on the initiative of Thomas Hales.
- Andrej Bauer (
@andrejbauer) - Mario Carneiro (
@digama0) - Floris van Doorn (
@fpvandoorn) - Kuen-Bang Hou (Favonia) (
@favonia) - Adam Kurkiewicz (
@picrin) - Robert Y. Lewis (
@rlewis1988)