home.social

#itp — Public Fediverse posts

Live and recent posts from across the Fediverse tagged #itp, aggregated by home.social.

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

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

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

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

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

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

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

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

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

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

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

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

  13. 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. isa-afp.org/entries/Dinitz_Gar #IsabelleHOL #ITP

  14. 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. isa-afp.org/entries/Dinitz_Gar #IsabelleHOL #ITP

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

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

  17. 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. arxiv.org/abs/2607.08986v2 #LeanProver #ITP #AI4Math

  18. 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. arxiv.org/abs/2607.08986v2 #LeanProver #ITP #AI4Math

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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