#CoqProver hashtag - Bluesky

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 month ago

Readings shared February 24, 2026 The readings shared in Bluesky on 24 February 2026 are: Formalizing Gröbner basis theory in Lean. ~ Junyu Guo, Hao Shen, Junqi Liu, Lihong Zhi. #LeanProver #ITP #Math Integral curves and flows on Ban

Readings shared February 24, 2026. jaalonso.github.io/vestigium/po... #AI4Math #ATP #Agda #CoqProver #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LLMs #LeanProver #Math #Reasoning #Vampire

1 0 0 0

José A. Alonso

@jalonso.eurosky.social

1 month ago

Verifying the Hashgraph Consensus Algorithm The Hashgraph consensus algorithm is an algorithm for asynchronous Byzantine fault tolerance intended for distributed shared ledgers. Its main distinguishing characteristic is it achieves consensus wi...

Verifying the hashgraph consensus algorithm. ~ Karl Crary. arxiv.org/abs/2102.011... #CoqProver #ITP

0 0 0 0

José A. Alonso

@jalonso.eurosky.social

1 month ago

Readings shared February 14, 2026 The readings shared in Bluesky on 14 February 2026 are: Formalization of the Golay-Hopf machine: A unified algebraic framework for Hida, Iwasawa, and Yang-Baxter structures. ~ Yoshihiro Hasegawa. #IT

Readings shared February 14, 2026. jaalonso.github.io/vestigium/po... #AI4Math #Agda #Clojure #CoqProver #FunctionalProgramming #Haskell #ITP #LeanProver #Lisp #Logic #Math #Minlog #Prolog #RustLang

0 0 0 0

José A. Alonso

@jalonso.eurosky.social

2 months ago

Mechanized Undecidability of Higher-order beta-Matching (Extended Version) Higher-order beta-matching is the following decision problem: given two simply typed lambda-terms, can the first term be instantiated to be beta-equivalent to the second term? This problem was formula...

Mechanized undecidability of higher-order beta-matching. ~ Andrej Dudenhefner. arxiv.org/abs/2602.02091 #ITP #CoqProver

0 0 0 0

José A. Alonso

@jalonso.eurosky.social

2 months ago

Readings shared January 24, 2026 The readings shared in Bluesky on 24 January 2026 are: Abel's limit theorem (in Isabelle/HOL). ~ Kangfeng Ye. #ITP #IsabelleHOL #Math A formalization of the downward Löwenheim-Skolem theorem in Coq.

Readings shared January 24, 2026. jaalonso.github.io/vestigium/po... #AI #AI4Math #ATP #CoqProver #HOL_Light #ITP #IsabelleHOL #LeanProver #Logic #Math #Prover9 #RocqProver

0 1 0 0

José A. Alonso

@jalonso.eurosky.social

2 months ago

AI for Mathematics: Progress, Challenges, and Prospects AI for Mathematics (AI4Math) has emerged as a distinct field that leverages machine learning to navigate mathematical landscapes historically intractable for early symbolic systems. While mid-20th-cen...

AI for mathematics: Progress, challenges, and prospects. ~ Haocheng Ju, Bin Dong. arxiv.org/abs/2601.132... #AI #Math #AI4Math #ITP #IsabelleHOL #CoqProver #LeanProver

0 0 0 0

José A. Alonso

@jalonso.eurosky.social

2 months ago

Blurred Drinker Paradoxes and Blurred Choice Axioms: Constructive Reverse Mathematics of the Downward Löwenheim-Skolem Theorem In the setting of constructive reverse mathematics, we analyse the downward Löwenheim-Skolem (DLS) theorem of first-order logic, stating that every infinite model has a countable elementary submodel. ...

Blurred drinker paradoxes and blurred choice axioms: Constructive reverse mathematics of the downward Löwenheim-Skolem theorem. ~ Dominik Kirst, Haoyi Zeng. arxiv.org/abs/2601.125... #ITP #CoqProver #Logic #Math

0 0 0 0

José A. Alonso

@jalonso.eurosky.social

2 months ago

A formalization of the downward Löwenheim-Skolem theorem in Coq. ~ Timothée Huneau. inria.hal.science/hal-05467238... #ITP #CoqProver #Logic #Math

0 0 0 0

José A. Alonso

@jalonso.eurosky.social

3 months ago

Readings shared December 29, 2025 The readings shared in Bluesky on 29 December 2025 are: Hint-based SMT proof reconstruction. ~ Joshua Clune, Haniel Barbosa, Jeremy Avigad. #ITP #LeanProver #SMT The biggest controversy in maths coul

Readings shared December 29, 2025. jaalonso.github.io/vestigium/po... #AI #Agda #CoqProver #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LeanProver #Logic #Math #OCaml #Rocq #SMT

1 0 0 0

José A. Alonso

@jalonso.eurosky.social

3 months ago

Readings shared December 7, 2025 The readings shared in Bluesky on 7 December 2025 are: 50 years of proof assistants. ~ Lawrence Paulson. #ITP #IsabelleHOL #CoqProver #HOL DeepWiki leanprover-community/mathlib4: A comprehensive data

Readings shared December 7, 2025. jaalonso.github.io/vestigium/po... #CoqProver #FunctionalProgramming #HOL #Haskell #ITP #IsabelleHOL #LeanProver #LogicProgramming #Math #Prolog #Python

1 0 0 0

José A. Alonso

@jalonso.eurosky.social

3 months ago

50 years of proof assistants. ~ Lawrence Paulson. lawrencecpaulson.github.io//2025/12/05/... #ITP #IsabelleHOL #CoqProver #HOL

0 0 0 0

José A. Alonso

@jalonso.eurosky.social

4 months ago

Readings shared December 2, 2025 The readings shared in Bluesky on 2 December 2025 are: The machine translation of Landau’s analysis of foundations in Rocq. ~ Yue Guan, Yaoshun Fu, XiangTao Meng. #ITP #Rocq #Math Formalization of br

Readings shared December 2, 2025. jaalonso.github.io/vestigium/po... #AI #CoqProver #ITP #IsabelleHOL #LLMs #LeanProver #Math #Rocq

0 0 0 0

José A. Alonso

@jalonso.eurosky.social

4 months ago

ProofGym: Unifying LLM-Based Theorem Proving Across Formal Systems Large language models (LLMs) have accelerated progress in automated theorem proving, but most systems remain confined to a single proof assistant, hindering cross-system reuse of reasoning patterns...

ProofGym: Unifying LLM-based theorem proving across formal systems. ~ Xinrui Li et als. openreview.net/forum?id=RrS... #ITP #LeanProver #IsabelleHOL #CoqProver #LLMs

1 1 0 0

José A. Alonso

@jalonso.eurosky.social

4 months ago

Readings shared November 24, 2025 The readings shared in Bluesky on 24 November 2025 are: An introduction to formal real analysis (Lecture 21: Functions and derivatives). ~ Alex Kontorovich. #ITP #LeanProver #Math A perspective on in

Readings shared November 24, 2025. jaalonso.github.io/vestigium/po... #CompSci #CoqProver #ITP #LeanProver #Logic #Math #Physics #SetTheory #TypeTheory

1 0 0 0

José A. Alonso

@jalonso.eurosky.social

4 months ago

A Coq-based Axiomatization of Tarski's Mereogeometry During the last decade, the domain of Qualitative Spatial Reasoning, has known a renewal of interest for mereogeometry, a theory that has been initiated by Tarski. Mereogeometry relies on mereology, t...

A Coq-based axiomatization of Tarski's mereogeometry. ~ Patrick Barlatier, Richard Dapoigny. arxiv.org/abs/2511.16705 #ITP #CoqProver

2 0 0 0

José A. Alonso

@jalonso.eurosky.social

4 months ago

A Topological Rewriting of Tarski's Mereogeometry Qualitative spatial models based on Goodman-style mereology and pseudo-topology often pose problems for advanced geometric reasoning, as they lack true Euclidean geometry and fully developed topologic...

A topological rewriting of Tarski's mereogeometry. ~ Patrick Barlatier, Richard Dapoigny. arxiv.org/abs/2511.127... #ITP #CoqProver

0 0 0 0

José A. Alonso

@jalonso.eurosky.social

4 months ago

Readings shared November 14, 2025 The readings shared in Bluesky on 14 November 2025 are: An introduction to formal real analysis (Lecture 18: Rearrangements). ~ Alex Kontorovich. #ITP #LeanProver #Math Choice trees: Representing and

Readings shared November 14, 2025. jaalonso.github.io/vestigium/po... #AI #Agda #AlphaProof #CoqProver #FunctionalProgramming #Haskell #ITP #LeanProver #Math #OCaml #Rocq

0 0 0 0

José A. Alonso

@jalonso.eurosky.social

4 months ago

A practical formalization of monadic equational reasoning in dependent-type theory | Journal of Functional Programming | Cambridge Core A practical formalization of monadic equational reasoning in dependent-type theory - Volume 35

A practical formalization of monadic equational reasoning in dependent-type theory. ~ Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa. www.cambridge.org/core/journal... #ITP #CoqProver

1 0 0 0

José A. Alonso

@jalonso.eurosky.social

5 months ago

Readings shared October 15, 2025 The readings shared in Bluesky on 15 October 2025 are: Rely-guarantee verification of queue locks with proof support in Isabelle/HOL. ~ Robert J. Colvin, Scott Heiner, Peter Höfner, Roger C. Su. #ITP

Readings shared October 15, 2025. jaalonso.github.io/vestigium/po... #AI #CoqProver #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LLMs #LeanProver #LiquidHaskell #Math #OCaml #Rocq

2 0 0 0

José A. Alonso

@jalonso.eurosky.social

5 months ago

Formal verification of COO to CSR sparse matrix conversion. ~ Andrew W. Appel. cgi.cse.unsw.edu.au/~eptcs/paper... #ITP #CoqProver

0 0 0 0

José A. Alonso

@jalonso.eurosky.social

5 months ago

Readings shared October 13, 2025 The readings shared in Bluesky on 13 October 2025 are: PVS formalization of proofs of the infinitude of primes. ~ Bruno Berto de Oliveira Ribeiro. #ITP #PVS #Math Certified decision procedures for wi

Readings shared October 13, 2025. jaalonso.github.io/vestigium/po... #Agda #CoqProver #Erlang #FunctionalProgramming #Haskell #ITP #LeanProver #Math #OCaml #PVS #Programming #Python #Rocq

3 0 0 0

José A. Alonso

@jalonso.eurosky.social

5 months ago

Pyrosome: Verified Compilation for Modular Metatheory | Proceedings of the ACM on Programming Languages We present Pyrosome, a generic framework for modular language metatheory that embodies a novel approach to extensible semantics and compilation, implemented in Coq. Common techniques for semantic reasoning are often tied to the specific structures of the ...

Pyrosome: Verified compilation for modular metatheory. ~ Dustin Jamner, Gabriel Kammer, Ritam Nag, Adam Chlipala. dl.acm.org/doi/10.1145/... #ITP #CoqProver

0 0 0 0

José A. Alonso

@jalonso.eurosky.social

5 months ago

Interactive Theorem Provers for Proof Education | Proceedings of the 2025 ACM SIGPLAN International Symposium on SPLASH-E

Interactive theorem provers for proof education. ~ Romina Mahinpei, Manoel Horta Ribeiro, Mae Milano. dl.acm.org/doi/abs/10.1... #ITP #CoqProver #Teaching

2 2 0 0

José A. Alonso

@jalonso.eurosky.social

5 months ago