#coqprover — Public Fediverse posts
Live and recent posts from across the Fediverse tagged #coqprover, aggregated by home.social.
-
Formalizing hyperspaces and operations on subsets of polish spaces over abstract exact real numbers. ~ Michal Konečný, Sewon Park, Holger Thies. https://arxiv.org/abs/2410.13508v1 #CoqProver #ITP #Math
-
Formalizing hyperspaces and operations on subsets of polish spaces over abstract exact real numbers. ~ Michal Konečný, Sewon Park, Holger Thies. https://arxiv.org/abs/2410.13508v1 #CoqProver #ITP #Math
-
A proof in Coq that core logic is not paraconsistent. ~ Joseph Vidal-Rosset. https://arxiv.org/abs/2606.05953v1 #CoqProver #ITP
-
A proof in Coq that core logic is not paraconsistent. ~ Joseph Vidal-Rosset. https://arxiv.org/abs/2606.05953v1 #CoqProver #ITP
-
Modelling and verifying neuronal archetypes in Coq. ~ Abdorrahim Bahrami, Rébecca Zucchini, Elisabetta De Maria, Amy Felty. https://arxiv.org/abs/2505.05362v1 #CoqProver #ITP
-
Modelling and verifying neuronal archetypes in Coq. ~ Abdorrahim Bahrami, Rébecca Zucchini, Elisabetta De Maria, Amy Felty. https://arxiv.org/abs/2505.05362v1 #CoqProver #ITP
-
Four paradoxes and a proof assistant: Burali-Forti, Diaconescu, Reynolds, and Hurkens in the coq-paradoxes library. ~ Bernardo Alonso. https://arxiv.org/abs/2605.27633v1 #CoqProver #ITP #Math
-
Four paradoxes and a proof assistant: Burali-Forti, Diaconescu, Reynolds, and Hurkens in the coq-paradoxes library. ~ Bernardo Alonso. https://arxiv.org/abs/2605.27633v1 #CoqProver #ITP #Math
-
Verified tableaux: from modal logics to modal fixpoint logics. https://link.springer.com/article/10.1007/s10817-026-09754-z #CoqProver #ITP #Logic
-
Verified tableaux: from modal logics to modal fixpoint logics. https://link.springer.com/article/10.1007/s10817-026-09754-z #CoqProver #ITP #Logic
-
Formal verification of Pohlig-Hellman algorithm for computing discrete logarithms with Coq. ~ Jeremiah Daniel A. Regalario et als. https://www.atlantis-press.com/article/126023793.pdf #CoqProver #ITP
-
Formal verification of Pohlig-Hellman algorithm for computing discrete logarithms with Coq. ~ Jeremiah Daniel A. Regalario et als. https://www.atlantis-press.com/article/126023793.pdf #CoqProver #ITP
-
Between Qed and truth (The permanent axiom trust boundary in machine-verified mathematics). ~ Ryan Christopher Fields. https://philarchive.org/archive/FIEBQA #CoqProver #ITP #Math
-
Between Qed and truth (The permanent axiom trust boundary in machine-verified mathematics). ~ Ryan Christopher Fields. https://philarchive.org/archive/FIEBQA #CoqProver #ITP #Math
-
Why not just use Lean?. ~ Lawrence Paulson. https://lawrencecpaulson.github.io//2026/04/23/Why_not_Lean.html #ITP #Nqthm #HOL #CoqProver #IsabelleHOL #LeanProver #AI4Math
-
Why not just use Lean?. ~ Lawrence Paulson. https://lawrencecpaulson.github.io//2026/04/23/Why_not_Lean.html #ITP #Nqthm #HOL #CoqProver #IsabelleHOL #LeanProver #AI4Math
-
Reseña de «AI for mathematical discovery (symbolic, neural and neuro-symbolic methods)». https://jaalonso.github.io/vestigium/posts/2025/07/11-ai-for-mathematical-discovery-symbolic-neural-and-neuro-symbolic-methods/ #AI4Math #ITP #LeanProver #IsabelleHOL #CoqProver
-
Reseña de «AI for mathematical discovery (symbolic, neural and neuro-symbolic methods)». https://jaalonso.github.io/vestigium/posts/2025/07/11-ai-for-mathematical-discovery-symbolic-neural-and-neuro-symbolic-methods/ #AI4Math #ITP #LeanProver #IsabelleHOL #CoqProver
-
Readings shared April 4, 2026. https://jaalonso.github.io/vestigium/posts/2026/04/04-readings_shared_04-04-26 #AI #AI4Math #ATP #Agda #AlphaProof #Autoformalization #CategoryTheory #CoqProver #FunctionalProgramming #ITP #IsabelleHOL #LLMs #LambdaCalculus #LeanProver #Lisp #Logic #LogicProgramming #LLMs #Math #Physics #Programming #Prolog #Racket #RocqProver #Vampire
-
Readings shared April 4, 2026. https://jaalonso.github.io/vestigium/posts/2026/04/04-readings_shared_04-04-26 #AI #AI4Math #ATP #Agda #AlphaProof #Autoformalization #CategoryTheory #CoqProver #FunctionalProgramming #ITP #IsabelleHOL #LLMs #LambdaCalculus #LeanProver #Lisp #Logic #LogicProgramming #LLMs #Math #Physics #Programming #Prolog #Racket #RocqProver #Vampire
-
Reseña de «50 years of proof assistants». https://jaalonso.github.io/vestigium/posts/2025/12/07-50-years-of-proof-assistants/ #ITP #IsabelleHOL #LeanProver #CoqProver
-
Reseña de «50 years of proof assistants». https://jaalonso.github.io/vestigium/posts/2025/12/07-50-years-of-proof-assistants/ #ITP #IsabelleHOL #LeanProver #CoqProver
-
A topological rewriting of Tarski’s mereogeometry. ~ Richard Dapoigny. https://hal.science/hal-05532641v1/file/RD_paper20381.pdf #CoqProver #ITP
-
A topological rewriting of Tarski’s mereogeometry. ~ Richard Dapoigny. https://hal.science/hal-05532641v1/file/RD_paper20381.pdf #CoqProver #ITP
-
Readings shared March 04, 2026. https://jaalonso.github.io/vestigium/posts/2026/03/05-readings_shared_02-04-26 #AI #AI4Math #CoqProver #FunctionalProgramming #Haskell #ITP #LeanProver #Math #RocqProver
-
Readings shared March 04, 2026. https://jaalonso.github.io/vestigium/posts/2026/03/05-readings_shared_02-04-26 #AI #AI4Math #CoqProver #FunctionalProgramming #Haskell #ITP #LeanProver #Math #RocqProver
-
A formally verified constructive proof of the consistency of Peano arithmetic using ordinal assignments. ~ Aaron Bryce, Rajeev Goré. https://arxiv.org/abs/2603.00487v1 #CoqProver #ITP #Math
-
A formally verified constructive proof of the consistency of Peano arithmetic using ordinal assignments. ~ Aaron Bryce, Rajeev Goré. https://arxiv.org/abs/2603.00487v1 #CoqProver #ITP #Math
-
Readings shared February 24, 2026. https://jaalonso.github.io/vestigium/posts/2026/02/25-readings_shared_02-24-26 #AI4Math #ATP #Agda #CoqProver #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LLMs #LeanProver #Math #Reasoning #Vampire
-
Readings shared February 24, 2026. https://jaalonso.github.io/vestigium/posts/2026/02/25-readings_shared_02-24-26 #AI4Math #ATP #Agda #CoqProver #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LLMs #LeanProver #Math #Reasoning #Vampire
-
Verifying the hashgraph consensus algorithm. ~ Karl Crary. https://arxiv.org/abs/2102.01167v1 #CoqProver #ITP
-
Verifying the hashgraph consensus algorithm. ~ Karl Crary. https://arxiv.org/abs/2102.01167v1 #CoqProver #ITP
-
Readings shared February 14, 2026. https://jaalonso.github.io/vestigium/posts/2026/02/15-readings_shared_02-14-26 #AI4Math #Agda #Clojure #CoqProver #FunctionalProgramming #Haskell #ITP #LeanProver #Lisp #Logic #Math #Minlog #Prolog #RustLang
-
Readings shared February 14, 2026. https://jaalonso.github.io/vestigium/posts/2026/02/15-readings_shared_02-14-26 #AI4Math #Agda #Clojure #CoqProver #FunctionalProgramming #Haskell #ITP #LeanProver #Lisp #Logic #Math #Minlog #Prolog #RustLang
-
Mechanized undecidability of higher-order beta-matching. ~ Andrej Dudenhefner. https://arxiv.org/abs/2602.02091 #ITP #CoqProver
-
Mechanized undecidability of higher-order beta-matching. ~ Andrej Dudenhefner. https://arxiv.org/abs/2602.02091 #ITP #CoqProver
-
Readings shared January 24, 2026. https://jaalonso.github.io/vestigium/posts/2026/01/25-readings_shared_01-24-26 #AI #AI4Math #ATP #CoqProver #HOL_Light #ITP #IsabelleHOL #LeanProver #Logic #Math #Prover9 #RocqProver
-
Readings shared January 24, 2026. https://jaalonso.github.io/vestigium/posts/2026/01/25-readings_shared_01-24-26 #AI #AI4Math #ATP #CoqProver #HOL_Light #ITP #IsabelleHOL #LeanProver #Logic #Math #Prover9 #RocqProver
-
AI for mathematics: Progress, challenges, and prospects. ~ Haocheng Ju, Bin Dong. https://arxiv.org/abs/2601.13209v2 #AI #Math #AI4Math #ITP #IsabelleHOL #CoqProver #LeanProver
-
AI for mathematics: Progress, challenges, and prospects. ~ Haocheng Ju, Bin Dong. https://arxiv.org/abs/2601.13209v2 #AI #Math #AI4Math #ITP #IsabelleHOL #CoqProver #LeanProver
-
Blurred drinker paradoxes and blurred choice axioms: Constructive reverse mathematics of the downward Löwenheim-Skolem theorem. ~ Dominik Kirst, Haoyi Zeng. https://arxiv.org/abs/2601.12592v1 #ITP #CoqProver #Logic #Math
-
Blurred drinker paradoxes and blurred choice axioms: Constructive reverse mathematics of the downward Löwenheim-Skolem theorem. ~ Dominik Kirst, Haoyi Zeng. https://arxiv.org/abs/2601.12592v1 #ITP #CoqProver #Logic #Math
-
A formalization of the downward Löwenheim-Skolem theorem in Coq. ~ Timothée Huneau. https://inria.hal.science/hal-05467238/file/thesis.pdf #ITP #CoqProver #Logic #Math
-
A formalization of the downward Löwenheim-Skolem theorem in Coq. ~ Timothée Huneau. https://inria.hal.science/hal-05467238/file/thesis.pdf #ITP #CoqProver #Logic #Math
-
Readings shared December 29, 2025. https://jaalonso.github.io/vestigium/posts/2025/12/30-readings_shared_12-29-25 #AI #Agda #CoqProver #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LeanProver #Logic #Math #OCaml #Rocq #SMT
-
Readings shared December 29, 2025. https://jaalonso.github.io/vestigium/posts/2025/12/30-readings_shared_12-29-25 #AI #Agda #CoqProver #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LeanProver #Logic #Math #OCaml #Rocq #SMT