Only github files/projects that provide formal marginalia for an article published in a journal whose website links to Marginis may appear in Marginis.

The Marginis entry of such a project can be cited simply by citing the original paper and adding “Marginis: Formal Marginalia #n for [paper citation]”, where n is the ordinal number of appearance in Marginis.

The following formalizations have not been refereed.

Formalizations in Lean, papers from Journal of Logic and Analysis:

1. Formal marginalia for Enlargements of schemes by Lars Brünjes and Christian Serpé, 2007.
2. Formal marginalia for Decomposition of terms in Lucas sequences
   by ABDELMADJID BOUDAOUD, 2009.
3. Formal marginalia for A computational aspect of the Lebesgue differentiation theorem by NOOPUR PATHAK, JLA 2009.
4. Formal marginalia for Localic completion of generalized metric spaces II: Powerlocales
   by STEVEN VICKERS, JLA 2009.
5. Formal marginalia for The probability distribution as a computational resource for randomness testing
   by BJØRN KJOS-HANSSEN, 2010.
6. Formal marginalia for Geometric spaces with no points by
   ROBERT S. LUBARSKY, JLA 2010.
7. Formal marginalia for Conway names, the simplicity hierarchy and the surreal number tree by
   PHILIP EHRLICH, JLA 2011.
8. Formal marginalia for Ends of groups: a nonstandard perspective by Isaac Goldbring, JLA 2011.
9. Formal marginalia for Unique paths as formal points by
   Thierry Coquand, Peter Schuster, JLA 2011.
10. Formal marginalia for Generating the Pfaffian closure with total Pfaffian functions
    by GARETH JONES and PATRICK SPEISSEGGER, 2012.
11. Formal marginalia for A constructive proof of Simpson’s Rule, by THIERRY COQUAND and BAS SPITTERS, JLA 2012.
12. Formal marginalia for Dorais, Hirst and Shafer’s Reverse mathematics, trichotomy, and dichotomy, JLA 2012.
13. Formal marginalia for A metastable dominated convergence theorem.
    Jeremy Avigad, Edward T Dean, Jason Rute. JLA, 2012.
14. Formal marginalia for Embedding an analytic equivalence relation in the transitive closure of a Borel relation by EDWARD J GREEN, 2013.
15. Formal marginalia for Discretisations of higher order and the theorems of Faa di Bruno and DeMoivre-Laplace
    by
    IMME VAN DEN BERG, JLA 2013.
16. Formal marginalia for Relative computability and uniform continuity of relations by
    Arno M Pauly, Martin A. Ziegler, JLA 2013.
17. Formal marginalia for First order irrationality criteria for series
    by LEE A. BUTLER, 2015.
18. Formal marginalia (by Clark Eggerman, Bjørn Kjos-Hanssen, S. Janani Lakshmanan, and Kawika O’Connor) for Limit laws and automorphism groups of random nonrigid structures by OVE AHLMAN and VERA KOPONEN, JLA 2015.
19. Formal marginalia for PFA and complemented subspaces of $\ell_{\infty}/c_0$ by ALAN DOW, 2016.
20. Formal marginalia for A Constructive Examination of Rectifiability by
    DOUGLAS S. BRIDGES
    MATTHEW HENDTLASS
    ERIK PALMGREN, JLA 2016.
21. Formal marginalia for Arno Pauly and Willem Fouche, How constructive is constructing measures?, 2017.
22. Formal marginalia for Abraham Robinson (6 October 1918 – 11 April 1974) by EDITORS, Journal of Logic & Analysis, 2018.
23. Formal marginalia for Randomness and Solovay degrees by Kenshi Miyabe, Andre Nies, and Frank Stephan, JLA 2018.
24. Formal marginalia for Constructive uniformities of pseudometrics and Bishop topologies by IOSIF PETRAKIS, JLA 2019.
25. Formal marginalia for Representation of Integers: A nonclassical point of view
    BOUDAOUD ABDELMADJID BELLAOUAR DJAMEL, JLA 2020.
26. Formal marginalia for Degrees of and lowness for isometric isomorphism by Johanna N.Y. Franklin and Timothy H. McNicholl, JLA 2020.
27. Formal marginalia for Integration with filters
    by
    Emanuele Bottazzi, Monroe Eskew, JLA 2022.
28. Formal marginalia for “Covering entropy for types in tracial $W^*$- algebras” by DAVID JEKEL, JLA 2023.
29. Formal marginalia for A computational study of a class of recursive inequalities by
    MORENIKEJI NERI
    and THOMAS POWELL, JLA 2023.

Formalizations in Isabelle, papers from Journal of Logic and Analysis:

1. Formal marginalia for A Lambda Calculus for Real Analysis by Paul Taylor.
2. Formal marginalia for Generalized effective completeness for continuous_logic by CALEB CAMRUD, 2023.