The readings shared in Bluesky on 23 March 2025 are

• A review on mechanical proving and formalization of mathematical theorems. ~ Si Chen, Wensheng Yu, Guowei Dou, Qimeng Zhang. #ITP #Coq #IsabelleHOL #HOL_Light #Mizar #LeanProver #Math
• Formalization of the axiom of choice and its equivalent theorems. ~ Tianyu Sun, Wensheng Yu (2019). #ITP #Coq #SetTheory
• A formal proof in Coq of Cantor-Bernstein-Schroeder’s theorem without axiom of choice (2019). #ITP #Coq #SetTheory
• A formal system of axiomatic set theory in Coq. ~ Tianyu Sun, Wensheng Yu (2020). #ITP #Coq #SetTheory
• A formalization of properties of continuous functions on closed intervals. Yaoshun Fu, Wensheng Yu (2020). #ITP #Coq #Math
• Formalization of the equivalence among completeness theorems of real number in Coq. ~ Yaoshun Fu, Wensheng Yu (2020). #ITP #Coq #Math
• Formalizing calculus without limit theory in Coq. ~ Yaoshun Fu, Wensheng Yu (2021). #ITP #Coq #Math
• A formalization of topological spaces in Coq. ~ Sheng Yan, Yaoshun Fu, Dakai Guo, and Wensheng Yu (2022). #ITP #Coq #Math #SetTheory
• Formalization of the filter extension principle (FEP) in Coq. ~ Guowei Dou, Wensheng Yu (2024). #ITP #Coq #Math #SetTheory
• Implementation of Bourbaki's elements of mathematics in Coq: Part one, theory of sets. ~ José Grimm (2009). #ITP #Coq #SetTheory
• Implementation of Bourbaki’s elements of mathematics in Coq: Part two, ordered sets, cardinals, integers. ~ José Grimm (2018). #ITP #Coq #Math
• Concurrent games in Agda. ~ Amy Yin. #ITP #Agda
• #Exercitium: Valores de polinomios representados con vectores. #Haskell #ProgramaciónFuncional #Matemáticas
• Demostraciones con Lean4 y con Isabelle/HOL de "s \ (t ∪ u) ⊆ (s \ t) \ u". #LeanProver #IsabelleHOL #Math #Calculemus