#itp — Public Fediverse posts

First-order methods for smooth convex optimization in Isabelle/HOL. ~ Feier Lyu. https://isa-afp.org/entries/Projected_Gradient_Descent.html #IsabelleHOL #ITP #Math

First-order methods for smooth convex optimization in Isabelle/HOL. ~ Feier Lyu. https://isa-afp.org/entries/Projected_Gradient_Descent.html #IsabelleHOL #ITP #Math

Deep Vision: A formal proof of Wolstenholmes theorem in Lean 4. ~ Alexandre Linhares. https://arxiv.org/abs/2604.16507v2 #LeanProver #ITP #AI4Math

Deep Vision: A formal proof of Wolstenholmes theorem in Lean 4. ~ Alexandre Linhares. https://arxiv.org/abs/2604.16507v2 #LeanProver #ITP #AI4Math

A proof of the Dittert conjecture in dimension 4 via an exact constrained sum-of-squares certificate. ~ Jinhui Li, Beibei Xiong, Zhengfeng Yang. https://arxiv.org/abs/2607.29191v2 #LeanProver #ITP #Math

A proof of the Dittert conjecture in dimension 4 via an exact constrained sum-of-squares certificate. ~ Jinhui Li, Beibei Xiong, Zhengfeng Yang. https://arxiv.org/abs/2607.29191v2 #LeanProver #ITP #Math

Machine-checked dual-write recovery from a committed log. ~ Andreas Andreakis. https://arxiv.org/abs/2608.00501 #IsabelleHOL #ITP

Machine-checked dual-write recovery from a committed log. ~ Andreas Andreakis. https://arxiv.org/abs/2608.00501 #IsabelleHOL #ITP

Lean 4.33.0 is live! https://lean-lang.org/doc/reference/latest/releases/v4.33.0/ #LeanProver #ITP

Lean 4.33.0 is live! https://lean-lang.org/doc/reference/latest/releases/v4.33.0/ #LeanProver #ITP

From the Dirichlet integral to Lobachevsky's formula: a formalization in Lean 4. ~ Daniel Goldberg, Antoine Vinciguerra. https://arxiv.org/abs/2608.07366v1 #LeanProver #ITP #Math

From the Dirichlet integral to Lobachevsky's formula: a formalization in Lean 4. ~ Daniel Goldberg, Antoine Vinciguerra. https://arxiv.org/abs/2608.07366v1 #LeanProver #ITP #Math

A formalization of the Laplace transform and its inversion in Lean 4. ~ Daniel Goldberg, Antoine Vinciguerra. https://arxiv.org/abs/2608.07384 #LeanProver #ITP #Math

A formalization of the Laplace transform and its inversion in Lean 4. ~ Daniel Goldberg, Antoine Vinciguerra. https://arxiv.org/abs/2608.07384 #LeanProver #ITP #Math

Readings shared: 3 – 9 August, 2026. https://jaalonso.github.io/vestigium/posts/2026/08/10-readings_shared_08-10-26 #AI #AI4Math #Coq #FormalVerification #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LeanProver #Logic #Math

Readings shared: 3 – 9 August, 2026. https://jaalonso.github.io/vestigium/posts/2026/08/10-readings_shared_08-10-26 #AI #AI4Math #Coq #FormalVerification #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LeanProver #Logic #Math

#RetoLean4: Enunciado del reto 14 (para todo n ∈ ℕ, 2n + 9 ≤ 2ⁿ⁺⁴). https://t.me/Retos_Matematicos/109557/142663 #LeanProver #ITP #Math

#RetoLean4: Enunciado del reto 14 (para todo n ∈ ℕ, 2n + 9 ≤ 2ⁿ⁺⁴). https://t.me/Retos_Matematicos/109557/142663 #LeanProver #ITP #Math

#Retolean4: Vídeo tutorial sobre cómo resolver el reto 13. https://youtu.be/EcNgDxgNya8 #LeanProver #ITP #Math

#Retolean4: Vídeo tutorial sobre cómo resolver el reto 13. https://youtu.be/EcNgDxgNya8 #LeanProver #ITP #Math

#RetoLean4: Soluciones del reto 13 (Desigualdad triangular inversa: ||x| - |y|| ≤ |x - y|). https://live.lean-lang.org/#url=https://github.com/jaalonso/Retos/blob/main/src/Reto_13.lean #LeanProver #ITP #Math

#RetoLean4: Soluciones del reto 13 (Desigualdad triangular inversa: ||x| - |y|| ≤ |x - y|). https://live.lean-lang.org/#url=https://github.com/jaalonso/Retos/blob/main/src/Reto_13.lean #LeanProver #ITP #Math

Game hopping in Lean. ~ Stefan Dziembowski, Grzegorz Fabiański, Daniele Micciancio, Rafał Stefański. https://arxiv.org/abs/2608.06261 #LeanProver #ITP

Game hopping in Lean. ~ Stefan Dziembowski, Grzegorz Fabiański, Daniele Micciancio, Rafał Stefański. https://arxiv.org/abs/2608.06261 #LeanProver #ITP

A formal counterexample to the cost-preserving single-source unsplittable flow conjecture (in Isabelle/HOL). ~ Arthur Freitas Ramos, David Barros Hulak, Ruy Jose Guerra Barretto de Queiroz. https://isa-afp.org/entries/Dinitz_Garg_Goemans_Counterexample.html #IsabelleHOL #ITP

A formal counterexample to the cost-preserving single-source unsplittable flow conjecture (in Isabelle/HOL). ~ Arthur Freitas Ramos, David Barros Hulak, Ruy Jose Guerra Barretto de Queiroz. https://isa-afp.org/entries/Dinitz_Garg_Goemans_Counterexample.html #IsabelleHOL #ITP

A deep embedding of HOL in HOL: soundness, completeness, consistency. ~ Christoph Benzmüller, Daniel Kirchner. https://isa-afp.org/entries/HOL_in_HOL_Deep.html #IsabelleHOL #ITP

A deep embedding of HOL in HOL: soundness, completeness, consistency. ~ Christoph Benzmüller, Daniel Kirchner. https://isa-afp.org/entries/HOL_in_HOL_Deep.html #IsabelleHOL #ITP

A formalization of the mean-field derivation of the Vlasov equation (Mathematician in the loop: AI-assisted Lean formalization as a strategy game). ~ Joseph K. Miller. https://arxiv.org/abs/2607.08986v2 #LeanProver #ITP #AI4Math

A formalization of the mean-field derivation of the Vlasov equation (Mathematician in the loop: AI-assisted Lean formalization as a strategy game). ~ Joseph K. Miller. https://arxiv.org/abs/2607.08986v2 #LeanProver #ITP #AI4Math

Topological semantics for scoped computational paths. ~ Arthur Freitas Ramos, Ruy J. G. B. de Queiroz, Anjolina Grisi de Oliveira, Tiago M. L. de Veras. https://arxiv.org/abs/2608.04228v1 #LeanProver #ITP #Math

Topological semantics for scoped computational paths. ~ Arthur Freitas Ramos, Ruy J. G. B. de Queiroz, Anjolina Grisi de Oliveira, Tiago M. L. de Veras. https://arxiv.org/abs/2608.04228v1 #LeanProver #ITP #Math

Every quasiperfect number has at least eight distinct prime factors. ~ Akira Toyohara, Ye Tao, Siqiong Yao. https://arxiv.org/abs/2608.02066v1 #LeanProver #ITP #AI4Math

Every quasiperfect number has at least eight distinct prime factors. ~ Akira Toyohara, Ye Tao, Siqiong Yao. https://arxiv.org/abs/2608.02066v1 #LeanProver #ITP #AI4Math

Verifying Verus: A Lean 4 formalization of the SST-to-AIR expression translation. ~ Shuge Rong. https://www.andrew.cmu.edu/user/avigad/Students/rong_ms_thesis.pdf #LeanProver #ITP

Verifying Verus: A Lean 4 formalization of the SST-to-AIR expression translation. ~ Shuge Rong. https://www.andrew.cmu.edu/user/avigad/Students/rong_ms_thesis.pdf #LeanProver #ITP

Fitting’s theorem and semirings of normal subgroups. ~ Damiano Testa. https://arxiv.org/abs/2607.29111v1 #LeanProver #ITP #AI4Math

Fitting’s theorem and semirings of normal subgroups. ~ Damiano Testa. https://arxiv.org/abs/2607.29111v1 #LeanProver #ITP #AI4Math

A bijective proof of a partition theorem of Berkovich and Uncu. ~ Michal Mogielnicki, Ken Ono, Niels Voss, Jujian Zhang. https://arxiv.org/abs/2608.05142v1 #AI4Math #LeanProver #ITP

A bijective proof of a partition theorem of Berkovich and Uncu. ~ Michal Mogielnicki, Ken Ono, Niels Voss, Jujian Zhang. https://arxiv.org/abs/2608.05142v1 #AI4Math #LeanProver #ITP

Isabelle: the last 40 years (and the next). ~ Lawrence Paulson. https://youtu.be/nEf-WVtpEek #IsabelleHOL #ITP

Isabelle: the last 40 years (and the next). ~ Lawrence Paulson. https://youtu.be/nEf-WVtpEek #IsabelleHOL #ITP

Completeness of the Q₀ higher-order logic (in Isabelle/HOL). ~ Asta Halkjær From, Jonathan Julian Huerta Munive, Anders Schlichtkrull. https://isa-afp.org/entries/Q0_Completeness.html #IsabelleHOL #ITP #Logic

Completeness of the Q₀ higher-order logic (in Isabelle/HOL). ~ Asta Halkjær From, Jonathan Julian Huerta Munive, Anders Schlichtkrull. https://isa-afp.org/entries/Q0_Completeness.html #IsabelleHOL #ITP #Logic

The Wallace-Simson line theorem in Isabelle/HOL. ~ Arthur Freitas Ramos, David Barros Hulak, Ruy Jose Guerra Barretto de Queiroz. https://isa-afp.org/entries/Simson.html #IsabelleHOL #ITP #Math

The Wallace-Simson line theorem in Isabelle/HOL. ~ Arthur Freitas Ramos, David Barros Hulak, Ruy Jose Guerra Barretto de Queiroz. https://isa-afp.org/entries/Simson.html #IsabelleHOL #ITP #Math

Lean4Lean: Verifying a typechecker for Lean, in Lean. ~ Mario Carneiro. https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2025.2 #LeanProver #ITP

Lean4Lean: Verifying a typechecker for Lean, in Lean. ~ Mario Carneiro. https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2025.2 #LeanProver #ITP

Lean refactor: Multi-objective controllable proof optimization via agentic strategy search. ~ Jialin Lu, Soonho Kong, Rodrigo Stehling, Kaiyu Yang, Zhangyang Wang. https://arxiv.org/abs/2605.20244 #LeanProver #ITP #AI4Math

Lean refactor: Multi-objective controllable proof optimization via agentic strategy search. ~ Jialin Lu, Soonho Kong, Rodrigo Stehling, Kaiyu Yang, Zhangyang Wang. https://arxiv.org/abs/2605.20244 #LeanProver #ITP #AI4Math

LeanCSP: A framework for certifying constraint reformulation and solving in Lean. ~ Pablo Manrique, Stefan Szeider. https://arxiv.org/abs/2607.28459v1 #LeanProver #ITP

LeanCSP: A framework for certifying constraint reformulation and solving in Lean. ~ Pablo Manrique, Stefan Szeider. https://arxiv.org/abs/2607.28459v1 #LeanProver #ITP

Formally certifying number field invariants. ~ Alain Chavarri Villarello, Sander R. Dahmen. https://arxiv.org/abs/2607.26230v1 #LeanProver #ITP #Math

Formally certifying number field invariants. ~ Alain Chavarri Villarello, Sander R. Dahmen. https://arxiv.org/abs/2607.26230v1 #LeanProver #ITP #Math

Verifying and generalizing simultaneous critical pairs. ~ René Thiemann. https://iwc2026.github.io/documents/iwc2026_proceedings.pdf#page=13 #IsabelleHOL #ITP #Math

Verifying and generalizing simultaneous critical pairs. ~ René Thiemann. https://iwc2026.github.io/documents/iwc2026_proceedings.pdf#page=13 #IsabelleHOL #ITP #Math

The Lean theorem prover: design, evolution, and impact. ~ Leo de Moura. https://leodemoura.github.io/static/floc26/ #LeanProver #ITP

The Lean theorem prover: design, evolution, and impact. ~ Leo de Moura. https://leodemoura.github.io/static/floc26/ #LeanProver #ITP

MechGeo: Autoformalizing and proving euclidean geometry in Lean 4. ~ Hao Shen, Junyu Guo, Tian Cui, Yuxuan Xiao, Lihong Zhi. https://arxiv.org/abs/2608.02295 #AI4Math #LeanProver #ITP

MechGeo: Autoformalizing and proving euclidean geometry in Lean 4. ~ Hao Shen, Junyu Guo, Tian Cui, Yuxuan Xiao, Lihong Zhi. https://arxiv.org/abs/2608.02295 #AI4Math #LeanProver #ITP