Semiring of Sets. - Roland Coghetto (Formaliz. Math., 2014)

Semiring of Sets: Examples. - Roland Coghetto (Formaliz. Math., 2014)

Some Facts about Trigonometry and Euclidean Geometry. - Roland Coghetto (Formaliz. Math., 2014)

Morley's Trisector Theorem. - Roland Coghetto (Formaliz. Math., 2015)

Finite Product of Semiring of Sets. - Roland Coghetto (Formaliz. Math., 2015)

Groups - Additive Notation. - Roland Coghetto (Formaliz. Math., 2015)

Convergent Filter Bases. - Roland Coghetto (Formaliz. Math., 2015)

Summable Family in a Commutative Group. - Roland Coghetto (Formaliz. Math., 2015)

Topology from Neighbourhoods. - Roland Coghetto (Formaliz. Math., 2015)

Tarski's Geometry and the Euclidean Plane in Mizar. - Adam Grabowski; Roland Coghetto (FM4M/MathUI/ThEdu/DP/WIP@CIKM, 2016)

Circumcenter, Circumcircle and Centroid of a Triangle. - Roland Coghetto (Formaliz. Math., 2016)

Altitude, Orthocenter of a Triangle and Triangulation. - Roland Coghetto (Formaliz. Math., 2016)

Cousin's Lemma. - Roland Coghetto (Formaliz. Math., 2016)

Chebyshev Distance. - Roland Coghetto (Formaliz. Math., 2016)

Double Sequences and Iterated Limits in Regular Space. - Roland Coghetto (Formaliz. Math., 2016)

Quasi-uniform Space. - Roland Coghetto (Formaliz. Math., 2016)

Uniform Space. - Roland Coghetto (Formaliz. Math., 2016)

Homography in ℝℙ. - Roland Coghetto (Formaliz. Math., 2016)

Tarski Geometry Axioms - Part II. - Roland Coghetto; Adam Grabowski (Formaliz. Math., 2016)

Topological structures as a tool for formal modelling of rough sets. - Adam Grabowski; Roland Coghetto (FedCSIS (Position Papers), 2017)

Group of Homography in Real Projective Plane. - Roland Coghetto (Formaliz. Math., 2017)

Pascal's Theorem in Real Projective Plane. - Roland Coghetto (Formaliz. Math., 2017)

Gauge Integral. - Roland Coghetto (Formaliz. Math., 2017)

Tarski Geometry Axioms. Part III. - Roland Coghetto; Adam Grabowski (Formaliz. Math., 2017)

Klein-Beltrami Model. Part I. - Roland Coghetto (Formaliz. Math., 2018)

Klein-Beltrami Model. Part II. - Roland Coghetto (Formaliz. Math., 2018)

Pythagorean Tuning: Pentatonic and Heptatonic Scale. - Roland Coghetto (Formaliz. Math., 2018)

Cross-Ratio in Real Vector Space. - Roland Coghetto (Formaliz. Math., 2019)

Tarski Geometry Axioms. Part IV - Right Angle. - Roland Coghetto; Adam Grabowski (Formaliz. Math., 2019)

Klein-Beltrami model. Part III. - Roland Coghetto (Formaliz. Math., 2020)

Klein-Beltrami model. Part IV. - Roland Coghetto (Formaliz. Math., 2020)

A Case Study of Transporting Urysohn's Lemma from Topology via Open Sets into Topology via Neighborhoods. - Roland Coghetto (Formaliz. Math., 2020)

Tarski's Parallel Postulate implies the 5th Postulate of Euclid, the Postulate of Playfair and the original Parallel Postulate of Euclid. - Roland Coghetto (Arch. Formal Proofs, 2021)

Pappus's Hexagon Theorem in Real Projective PlaneThis work has been supported by the "Centre autonome de formation et de recherche en mathématiques et sciences avec assistants de preuve" ASBL (non-profit organization). Enterprise number: 0777.779.751. Belgium. - Roland Coghetto (Formaliz. Math., 2021)

Duality Notions in Real Projective Plane. - Roland Coghetto (Formaliz. Math., 2021)

Non-Trivial Universes and Sequences of Universes. - Roland Coghetto (Formaliz. Math., 2022)

Tarski Geometry Axioms. Part V - Half-planes and Planes. - Roland Coghetto; Adam Grabowski (Formaliz. Math., 2023)

U-Small and U-Locally Small Categories. - Roland Coghetto (Formaliz. Math., 2024)