Embracing AI and formalization: Experimenting with tomorrow’s mathematical tools. ~ Jarod Alper. pubs.ams.org/BULL/0000-00... #AI4Math #LeanProver #ITP #Math

Formally verifying digital circuits with category theory in Lean. ~ Matt Hunzinger. matt.hunzinger.me/2026/03/28/c... #LeanProver #ITP #CategoryTheory

A Lean formalisation of sphere packing in dimension 8. ~ Siddharth Hariharan. tube.switch.ch/videos/NHXRC... #LeanProver #ITP #Math

Formalizing the sphere packing problem. ~ Maryna Viazovska. tube.switch.ch/videos/ggmRt... #LeanProver #ITP #Math

Lean: Collaboration using formalization. ~ Floris van Doorn. tube.switch.ch/videos/AftiL... #LeanProver #ITP #Math

Shaping the future of mathematics in the age of AI. ~ Johan Commelin, Mateja Jamnik, Rodrigo Ochigame, Lenny Taelman, Akshay Venkatesh. www.math.ias.edu/~akshay/mnot... #AI4Math #LeanProver #ITP

Executable Gödel encodings: A verified runtime for logical syntax. ~ Adrian Diamond. aadsystems.com/papers/godel... #LeanProver #ITP #Logic #Math

On the paucity of lattice triangles A rational triangle $T$ (one whose angles are rational multiples of $π$) unfolds to a translation surface $(X_T,ω_T)$. The lattice triangle problem asks to classify those $T$ for which $(X_T,ω_T)$ is ...

On the paucity of lattice triangles. ~ David Kurniadi Angdinata, Evan Chen, Ken Ono, Jiaxin Zhang, Jujian Zhang. arxiv.org/abs/2603.239... #LeanProver #ITP #Math

Daratumumab in patients with immune thrombocytopenia: a single-center, open-label, phase 2 trial

These findings suggest that daratumumab could be a potential therapeutic option for adults with immune thrombocytopenia

www.thelancet.com/journals/ecl...
#ITP #ImmuneThrombocytopenia #HaemSky #MedSky

Readings shared March 24, 2026 The readings shared in Bluesky on 24 March 2026 are: Synthetic differential geometry in Lean. ~ Riccardo Brasca, Gabriella Clemente. #LeanProver #ITP #Math The spectral comb and the Riemann hypothesi

Readings shared March 24, 2026. jaalonso.github.io/vestigium/po... #AI4Math #Autoformalization #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LeanProver #Math

AI-Predicting Compound Affinity. We Aren't There Yet.

The #ItP view on #ML binding affinity prediction #DrugDesign #MedChem #CompChem #cheminformatics #AI #chemsky 🧪

“Unfortunately, we don’t spend much time on Easy Mode in the wonder drug factories”

www.science.org/content/blog...

A quote on a blue textured background reads, "I have to remind myself every day that I have no control over what my body does. I’ve been here before, and I’m positive I’ll be here again. It wasn’t worth the tears this time." Below, there is a circular photo of a person with glasses and a smile. The name "Kristy Coleman" and the title "ITP Contributor" are included.

In her latest patient perspective column, Kristy Coleman opens up about navigating the emotional highs and lows of living with immune thrombocytopenia (#ITP).

Read Kristy's full column 🖊️: https://bit.ly/41n7a6v

#RareDisease #RareVoices #PatientPerspectives #MedSky

A formal embedding for assessing the complexity of model consistency. ~ Romain Pascual et als. assets-eu.researchsquare.com/files/rs-897... #IsabelleHOL #ITP

Sorted Rewriting, Conditional Rewriting, and Logically Constrained Rewriting Sorted Rewriting, Conditional Rewriting, and Logically Constrained Rewriting in the Archive of Formal Proofs

Sorted rewriting, conditional rewriting, and logically constrained rewriting (in Isabelle/HOL). ~ Akihisa Yamada. www.isa-afp.org/entries/Sort... #IsabelleHOL #ITP

Lebesgue-Stieltjes Integral Lebesgue-Stieltjes Integral in the Archive of Formal Proofs

Lebesgue-Stieltjes integral (in Isabelle/HOL). ~ Yosuke Ito. www.isa-afp.org/entries/Lebe... #IsabelleHOL #ITP #Math

OpenGauss: an open source, state of the art autoformalization harness — Math, Inc. OpenGauss is a state-of-the-art open-source autoformalization harness for Lean, built for practical proof engineering workflows.

OpenGauss: an open source, state of the art autoformalization harness. www.math.inc/opengauss #AI4Math #LeanProver #ITP #Autoformalization

Code Proven to Work - The Math Way This post is aimed at a general programmer and no prior knowledge of math or CS is assumed. I got nerd-sniped to write this after reading Simon’s excellent post Code proven to work. As someone who wor...

Rado's radical reflections. ~ Rado Kirov. rkirov.github.io/posts/code-p... #LeanProver #ITP #FunctionalProgramming

Semi-Autonomous Formalization of the Vlasov-Maxwell-Landau Equilibrium We present a complete Lean 4 formalization of the equilibrium characterization in the Vlasov-Maxwell-Landau (VML) system, which describes the motion of charged plasma. The project demonstrates the ful...

Semi-autonomous formalization of the Vlasov-Maxwell-Landau equilibrium. ~ Vasily Ilin. arxiv.org/abs/2603.159... #LeanProver #ITP

Formalizing the Classical Isoperimetric Inequality in the Two-Dimensional Case We present a formal verification of the classical isoperimetric inequality in the plane using the Lean 4 proof assistant and its mathematical library Mathlib. We follow Adolf Hurwitz's analytic approa...

Formalizing the classical isoperimetric inequality in the two-dimensional case. ~ Miraj Samarakkody. arxiv.org/abs/2603.146... #LeanProver #ITP #Math

The spectral comb and the Riemann hypothesis: A proof via fixed-point theory. ~ Engin Atik. kleis.io/docs/papers/... #LeanProver #ITP #Math

Synthetic differential geometry in Lean. ~ Riccardo Brasca, Gabriella Clemente. hal.science/hal-05555752... #LeanProver #ITP #Math

The Best Weapon Yet Against Sleeping Sickness

Good news in the fight against African trypanosomiasis (sleeping sickness) #ITP #DrugDiscovery #MedChem #boron #chemsky 🧪
www.science.org/content/blog...

Readings shared March 19, 2026 The readings shared in Bluesky on 19 March 2026 are: Aristotle: The World's most advanced formal reasoning agent. #LeanProver #ITP #Math Formalization of QFT (quantum field theory). ~ Michael R. Doug

Readings shared March 19, 2026. jaalonso.github.io/vestigium/po... #ATP #ITP #IsabelleHOL #LLMs #LeanProver #Logic #Math #Physics #Prover9

Formal Verification of Axiom-Free Gödelian Ontological Argument and Trinity Necessity Proof in Isabelle HOL Formal Verification of Axiom-Free Gödelian Ontological Argument and Trinity Necessity Proof in Isabelle HOL in the Archive of Formal Proofs

Formal verification of axiom-free gödelian ontological argument and trinity necessity proof in Isabelle HOL. ~ Yong-Dock Kim. www.isa-afp.org/entries/Axio... #IsabelleHOL #ITP

Synthetic Differential Geometry in Lean This article is about the formalization of synthetic differential geometry with the Lean proof assistant and the mathematical library mathlib. The main result we prove and formalize is a Taylor theore...

Synthetic differential geometry in Lean. ~ Riccardo Brasca, Gabriella Clemente. arxiv.org/abs/2603.17457 #LeanProver #ITP #Math

Formalizing the Classical Isoperimetric Inequality in the Two-Dimensional Case We present a formal verification of the classical isoperimetric inequality in the plane using the Lean 4 proof assistant and its mathematical library Mathlib. We follow Adolf Hurwitz's analytic approa...

Formalizing the classical isoperimetric inequality in the two-dimensional case. ~ Miraj Samarakkody. arxiv.org/abs/2603.146... #LeanProver #ITP #Math

Formalization of QFT A foundational result in constructive quantum field theory is the construction of the free bosonic quantum field theory in four-dimensional Euclidean spacetime and the proof that it satisfies the Glim...

Formalization of QFT (quantum field theory). ~ Michael R. Douglas, Sarah Hoback, Anna Mei, Ron Nissim. arxiv.org/abs/2603.157... #LeanProver #ITP #Physics

Aristotle: The World's most advanced formal reasoning agent. aristotle.harmonic.fun #LeanProver #ITP #Math

Readings shared March 14, 2026 The readings shared in Bluesky on 14 March 2026 are: From SMT solvers to Lean and the future of automated reasoning. ~ Leo de Moura, Nicola Gigante. #LeanProver #ITP A formalization of Borel determin

Readings shared March 14, 2026. jaalonso.github.io/vestigium/po... #AI #Agda #ITP #LeanProver #Math #Mizar

Formalization of separable version of Banach–Alaoglu theorem. ~ Hiroyuki Okazaki, Takehiko Mieno. reference-global.com/download/art... #Mizar #ITP #Math