formalization

my own formalized results

• Formalization of results from Flimsy Spaces (Proposition 4.1 (C3), Proposition 3.8, Lemma 3.11, Theorem 3.13):
  • In Lean 4 (2025)
• Formalization of results from Study of a division-like property (Proposition 2.1, Theorem 2.2, Theorem 2.6):
  • In Lean 4 (2023)
  • In Lean 3 (2022)

links

• XenaProject
• The Natural Number Game

• Lean Zulip

• The 1Lab for cubical type theory
• TypeTopology
• Dedukti
• The Four Color Theorem in Coq, The Independence of the Continuum Hypothesis in Lean, \(\pi_4(\mathbb{S}^3)\) in HoTT/Cubical Agda, Feit-Thompson in Coq, Liquid Tensor Experiment
• Fermat’s Last Theorem: n = 3 in Lean, n ∈ {3, 4} in Isabelle