#itp

@jalonso.eurosky.social

2 hours ago

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

0 0 0 0

José A. Alonso

@jalonso.eurosky.social

14 hours ago

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

0 0 0 0

José A. Alonso

@jalonso.eurosky.social

14 hours ago

Formalization of Wallis infinite product formula for π and the Wallis integral. ~ Yasushige Watase. reference-global.com/download/art... #Mizar #ITP #Math

0 0 0 0

José A. Alonso

@jalonso.eurosky.social

14 hours ago

Optimal Caverna Gameplay via Formal Methods - Stephen Diehl Personal blog of Stephen Diehl - Software engineer writing about technology, programming, and the future

Optimal Caverna gameplay via formal methods. ~ Stephen Diehl. www.stephendiehl.com/posts/caverna/ #LeanProver #ITP

0 1 0 0

José A. Alonso

@jalonso.eurosky.social

14 hours ago

Duality theory in linear optimization and its extensions -- formally verified Farkas established that a system of linear inequalities has a solution if and only if we cannot obtain a contradiction by taking a linear combination of the inequalities. We state and formally prove several Farkas-like theorems over linearly ordered fields in Lean 4. Furthermore, we extend duality theory to the case when some coefficients are allowed to take "infinite values".

Duality theory in linear optimization and its extensions - formally verified. ~ Martin Dvorak, Vladimir Kolmogorov. afm.episciences.org/17678 #LeanProver #ITP #Math

1 0 0 0

José A. Alonso

@jalonso.eurosky.social

14 hours ago

A formalization of Borel determinacy in Lean We present a formalization of Borel determinacy in the Lean 4 theorem prover. The formalization includes a definition of Gale-Stewart games and a proof of Martin's theorem stating that Borel games are determined. The proof closely follows Martin's "A purely inductive proof of Borel determinacy".

A formalization of Borel determinacy in Lean. ~ Sven Manthe. afm.episciences.org/17712 #LeanProver #ITP #Math

0 0 0 0

José A. Alonso

@jalonso.eurosky.social

14 hours ago

From SMT Solvers to Lean and the Future of Automated Reasoning Interview with Leo De Moura about his career and his work on Lean.

From SMT solvers to Lean and the future of automated reasoning. ~ Leo de Moura, Nicola Gigante. etaps.org/blog/043-leo... #LeanProver #ITP

2 1 0 0

Lexpro Asesoría

@luzdivinamorera.bsky.social

2 days ago

Liquidación del Impuesto de Transmisiones Patrimoniales (ITP). 💸 No pagues de más en la compra de tu coche o vivienda de segunda mano. 🚗 Gestionamos tus impuestos con rigor. 🏠 #ITP #Impuestos #Gestoría

0 0 0 0

José A. Alonso

@jalonso.eurosky.social

4 days ago

Readings shared March 9, 2026 The readings shared in Bluesky on 9 March 2026 are: Fantastic simprocs and how to write them. ~ Yaël Dillies, Paul Lezeau. #LeanProver #ITP Formalization in Lean of faithfully flat descent of project

Readings shared March 09, 2026. jaalonso.github.io/vestigium/po... #AI #AI4Math #CategoryTheory #CoqProver #Emacs #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LambdaCalculus #LeanProver #Lisp #Math #Physics #RocqProver

2 0 0 0

José A. Alonso

@jalonso.eurosky.social

4 days ago

Fantastic Simprocs and How to Write Them How to write a simproc in practice

Fantastic simprocs and how to write them. ~ Yaël Dillies, Paul Lezeau. leanprover-community.github.io/blog/posts/s... #LeanProver #ITP

7 1 0 0

José A. Alonso

@jalonso.eurosky.social

5 days ago

A topological rewriting of Tarski’s mereogeometry. ~ Richard Dapoigny. hal.science/hal-05532641... #CoqProver #ITP

0 0 0 0

José A. Alonso

@jalonso.eurosky.social

5 days ago

Formalizing the stability of the two Higgs doublet model potential into Lean: identifying an error in the literature In 2006, using the best methods and techniques available at the time, Maniatis, von Manteuffel, Nachtmann and Nagel published a now widely cited paper on the stability of the two Higgs doublet model (...

Formalizing the stability of the two Higgs doublet model potential into Lean: identifying an error in the literature. ~ Joseph Tooby-Smith. arxiv.org/abs/2603.081... #LeanProver #ITP #Physics

2 1 0 0

José A. Alonso

@jalonso.eurosky.social

5 days ago

Apply2Isar: Automatically Converting Isabelle/HOL Apply-Style Proofs to Structured Isar In Isabelle/HOL, declarative proofs written in the Isar language are widely appreciated for their readability and robustness. However, some users may prefer writing procedural "apply-style" proof scri...

Apply2Isar: Automatically converting Isabelle/HOL apply-style proofs to structured Isar. ~ Sage Binder, Hanna Lachnitt, Katherine Kosaian. arxiv.org/abs/2603.077... #IsabelleHOL #ITP

0 0 0 0

José A. Alonso

@jalonso.eurosky.social

5 days ago

Implementing Dependent Type Theory Inhabitation and Unification Dependent type theory is the foundation of many modern proof assistants. Inhabitation and unification are undecidable problems that are useful for theorem proving and program synthesis. We introduce C...

Implementing dependent type theory inhabitation and unification. ~ Chase Norman, Jeremy Avigad. arxiv.org/abs/2603.01463 #LeanProver #ITP

4 1 0 0

José A. Alonso

@jalonso.eurosky.social

5 days ago

Unbiasing symmetric monoidal categories in Lean We present a formalization in Lean 4, within the framework of the mathematical library Mathlib, of the unbiasing process for symmetric monoidal categories. This is realized by extending the data of a ...

Unbiasing symmetric monoidal categories in Lean. ~ Robin Carlier. arxiv.org/abs/2603.00896 #LeanProver #ITP

1 0 0 0

José A. Alonso

@jalonso.eurosky.social

5 days ago

Mathematicians in the age of AI Recent developments show that AI can prove research-level theorems in mathematics, both formally and informally. This essay urges mathematicians to stay up-to-date with the technology, to consider the...

Mathematicians in the age of AI. ~ Jeremy Avigad. arxiv.org/abs/2603.03684 #AI4Math #LeanProver #ITP

0 0 0 0

José A. Alonso

@jalonso.eurosky.social

5 days ago

Formalization in Lean of faithfully flat descent of projectivity We formalize in Lean the following foundational result in commutative algebra: Let $R \to S$ be a faithfully flat map of (not necessarily noetherian) commutative rings, and let $P$ be an arbitrary $R$...

Formalization in Lean of faithfully flat descent of projectivity. ~ Liran Shaul. arxiv.org/abs/2603.04376 #LeanProver #ITP

1 0 0 0

José A. Alonso

@jalonso.eurosky.social

5 days ago

Proving and Computing: The Infinite Pigeonhole Principle and Countable Choice Structural recursion is a common technique used by programmers in modern languages and is taught to introductory computer science students. But what about its dual, structural corecursion? Structural ...

Proving and computing: The infinite pigeonhole principle and countable choice. ~ Zena M. Ariola, Paul Downen, Hugo Herbelin. arxiv.org/abs/2603.04006 #RocqProver #ITP

0 0 0 0

José A. Alonso

@jalonso.eurosky.social

5 days ago

Formalizing unstable quasinormal modes and the quantum black hole bomb in Lean 4. ~ Naoki Takata. naokitakata.com/quantum_supe... #ITP #LeanProver

0 0 0 0

José A. Alonso

@jalonso.eurosky.social

5 days ago

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

0 0 0 0

José A. Alonso

@jalonso.eurosky.social

5 days ago

LeanTutor: A Formally-Verified AI Tutor for Mathematical Proofs We present LeanTutor, a Large Language Model (LLM)-based tutoring system for math proofs. LeanTutor interacts with the student in natural language, formally verifies student-written math proofs in Lea...

LeanTutor: A formally-verified AI tutor for mathematical proofs. ~ Manooshree Patel, Rayna Bhattacharyya, Thomas Lu, Arnav Mehta, Niels Voss, Narges Norouzi, Gireeja Ranade. arxiv.org/abs/2506.083... #LeanProver #ITP #Math #AI4Math

1 0 0 0

José A. Alonso

@jalonso.eurosky.social

5 days ago

Formalizing a proof in Lean using Claude Code YouTube video by Terence Tao

Formalizing a proof in Lean using Claude Code. ~ Terence Tao. youtu.be/JHEO7cplfk8 #LeanProver #ITP #AI4Math

3 0 1 0

Rare Disease Advisor

@rarediseaseadvisor.bsky.social

6 days ago

ITP Associated With Depression Via MR Analysis Researchers found a genetically causal positive association between primary immune thrombocytopenia (ITP) and depression.

Researchers found a genetically causal association between primary immune thrombocytopenia (#ITP) and #Depression, but not #Anxiety. Study in Journal of Clinical Laboratory Analysis.

Read more: https://bit.ly/3MWMdvL

#RareDisease #MedSky #ImmuneThrombocytopenia

3 1 0 0

José A. Alonso

@jalonso.eurosky.social

1 week ago

Readings shared March 4, 2026 The readings shared in Bluesky on 4 March 2026 are: When AI writes the world’s software, who verifies it? ~ Leonardo de Moura. #AI #LeanProver #ITP Formalising sphere packing in Lean. ~ Chris Birkbec

Readings shared March 04, 2026. jaalonso.github.io/vestigium/po... #AI #AI4Math #CoqProver #FunctionalProgramming #Haskell #ITP #LeanProver #Math #RocqProver

1 0 0 0

José A. Alonso

@jalonso.eurosky.social

1 week ago

ReasBook is a Lean 4 project for formalizing mathematics from textbooks and research papers. github.com/optpku/ReasB... #LeanProver #ITP #Math

2 2 0 0

José A. Alonso

@jalonso.eurosky.social

1 week ago

Mechanizing the proof of a borrow calculus. ~ Alban Reynaud Michez. hal.science/hal-05527340... #RocqProver #ITP

0 0 0 0

José A. Alonso

@jalonso.eurosky.social

1 week ago

DRAFT: A Formally Verified Constructive Proof of the Consistency of Peano Arithmetic Using Ordinal Assignments Gentzen's 1936 proof of the consistency of Peano Arithmetic was a significant result in the foundations of mathematics. We provide here a modified version of the proof, based on Gödel's reformulatio...

A formally verified constructive proof of the consistency of Peano arithmetic using ordinal assignments. ~ Aaron Bryce, Rajeev Goré. arxiv.org/abs/2603.004... #CoqProver #ITP #Math

0 0 0 0

José A. Alonso

@jalonso.eurosky.social

1 week ago

SorryDB: Can AI Provers Complete Real-World Lean Theorems? We present SorryDB, a dynamically-updating benchmark of open Lean tasks drawn from 78 real world formalization projects on GitHub. Unlike existing static benchmarks, often composed of competition prob...

SorryDB: Can AI provers complete real-world Lean theorems? ~ Austin Letson et als. arxiv.org/abs/2603.026... #LeanProver #ITP #AI

2 1 0 1

José A. Alonso

@jalonso.eurosky.social

1 week ago

The Purpose of Proofs In discussions of AI and Mathematics, the discussion often goes to mathematical proofs, such as the the First Proof challenge. So let's lo...

The purpose of proofs. ~ Lance Fortnow. blog.computationalcomplexity.org/2026/03/the-... #LeanProver #ITP #AI4Math