#prover9 — Public Fediverse posts

Readings shared April 9, 2026. https://jaalonso.github.io/vestigium/posts/2026/04/10-readings_shared_04-09-26 #AI #AI4Math #ATP #Agda #FunctionalProgramming #ITP #IsabelleHOL #LeanProver #Math #Prover9

An optimal 14-symbol hybrid basis for BCH-algebras. ~ Mahesh Ramani, Shlok Kumar. https://arxiv.org/abs/2603.29137v1 #Prover9 #ATP #Math

Readings shared March 19, 2026. https://jaalonso.github.io/vestigium/posts/2026/03/20-readings_shared_02-19-26 #ATP #ITP #IsabelleHOL #LLMs #LeanProver #Logic #Math #Physics #Prover9

In the mood for inference: Logic-based natural language inference with large language models. ~ Bill Noble, Rasmus Blanck, Gijs Wijnholds. https://scholarlypublications.universiteitleiden.nl/access/item%3A4294827/download #Prover9 #ATP #LLMs

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

Elementary proofs of ring commutativity theorems. ~ Michael Kinyon, Desmond MacHale. https://arxiv.org/abs/2601.12599v1 #ATP #Prover9 #Math

Readings shared July 12, 2025. https://jaalonso.github.io/vestigium/posts/2025/07/13-readings_shared_07-12-25 #ASP #ATP #CLP #CategoryTheory #CoqProver #Emacs #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LLMs #LeanProver #Logic #LogicProgramming #Math #Prolog #ProofTheory #Prover9

Marginal subsemigroups and commutators in inverse semigroups. ~ Gonçalo Araújo, João Araújo, Michael Kinyon https://link.springer.com/article/10.1007/s00233-025-10548-9 #ATP #Prover9 #Math

Readings shared June 10, 2025. https://jaalonso.github.io/vestigium/posts/2025/06/11-readings_shared_06-10-25 #AI #AIforMath #ATP #AlphaProof #Emacs #ITP #IsabelleHOL #LLMs #LeanProver #Math #Prover9

Are LLMs reliable translators of logical reasoning across lexically diversified contexts? ~ Qingchuan Li et als. https://arxiv.org/abs/2506.04575v1 #LLMs #Math #ATP #Prover9

Readings shared April 13, 2025. https://jaalonso.github.io/vestigium/posts/2025/04/13-readings_shared_04-13-25 #AI #ATP #Coq #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LLMs #LeanProver #Mace4 #Math #Prover9 #SetTheory

Curso "Razonamiento automático (2011-12)". https://jaalonso.github.io/cursos/m-ra-11 #RazonamientoAutomático #Otter #Mace2 #Prover9 #Mace4 #DemostraciónInteractiva #IsabelleHOL

Readings shared March 24, 2025. https://jaalonso.github.io/vestigium/posts/2025/03/24-readings_shared_03-24-25 #AI #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LLMs #LeanProver #Lisp #LogicProgramming #MachineLearning #Math #Otter #Prolog #Prover9

Curso "Razonamiento automático (2008-09)". https://jaalonso.github.io/cursos/d-ra-08 #RazonamientoAutomático #Otter #Mace2 #Prover9 #Mace4 #DemostraciónInteractiva #IsabelleHOL

Readings shared March 18, 2025. https://jaalonso.github.io/vestigium/posts/2025/03/18-readings_shared_03-18-25 #AI #ASP #ATP #CLP #CommonLisp #Datalog #FunctionalProgramming #Haskell #ITP #IsabelleHOL #Logic #LogicProgramming #Mace #Math #Otter #Prolog #Prover9 #SMT #Z3

Curso "Razonamiento automático (2007-08)". https://jaalonso.github.io/cursos/d-ra-07 #RazonamientoAutomático #Otter #Mace2 #Prover9 #Mace4 #DemostraciónInteractiva #IsabelleHOL

Readings shared February 23, 2025. https://jaalonso.github.io/vestigium/posts/2025/02/23-readings_shared_02-23-25 #ATP #Coq #ITP #IsabelleHOL #Mace4 #Math #Mizar #Prover9 #Rocq

Fracterm calculus for partial meadows. ~ Jan A. Bergstra, Alban Ponse. https://arxiv.org/abs/2502.13812 #ATP #Prover9 #Mace4 #Math

Readings shared December 13, 2024. https://jaalonso.github.io/vestigium/posts/2024/12/13-readings_shared_12-13-24 #ITP #IsabelleHOL #Coq #Rocq #ATP #Prover9 #Mace4 #Logic #Math

Univocity of intuitionistic and classical connectives. ~ Rodolfo C. Ertola-Biraben, Branden Fitelson. https://philarchive.org/archive/FITUOI #ATP #Prover9 #Mace4 #Logic #Math

Long Hei Matthew Lam from Monash University has given the oral presentation titled A Closer Look at Tool-based Logical Reasoning with #LLMs: The Choice of Tool Matters.

In this paper, he fills the gaps in the comparison between symbolic solvers, including #Z3, #Pyke, and
#Prover9 with #LLMs augmented.

Readings shared September 20, 2024. https://jaalonso.github.io/vestigium/posts/2024/09/20-readings_shared_09-20-24 #ITP #Lean4 #IsabelleHOL #Math #Calculemus #ATP #Prover9 #Mace4

Mapping probability with logic: First order models in puzzle solving. ~ Adrian Groza. https://www.uni.lodz.pl/fileadmin/Projekty/EXTENDD/abstracts.pdf#page=18 #ATP #Prover9 #Mace4

Readings shared September 7, 2024. https://jaalonso.github.io/vestigium/posts/2024/09/07-readings_shared_09-07-24 #ITP #Lean4 #IsabelleHOL #Maude #ATP #Prover9 #Math #Calculemus

First-order theorem proving with power maps in semigroups. ~ Yi Lin1, Ranganathan Padmanabhan & Yang Zhang. https://ceur-ws.org/Vol-3754/paper11.pdf #ATP #Prover9 #Math

prover9 was last released in 2009. Nixpkgs has it, and it works out of the box. very satisfying.

#nix #prover9

Lecturas compartidas el 7 de junio de 2024. https://jaalonso.github.io/vestigium/posts/2024/06/08-lecturas_compartidas_el_07-jun-24 #ITP #Lean4 #IsabelleHOL #PVS #Math #ATP #Prover9 #SMT #Z3 #FunctionalProgramming #Haskell #LLMs

A closer look at logical reasoning with LLMs: The choice of tool matters. ~ Long Hei Matthew Lam, Ehsan Shareghi. https://arxiv.org/abs/2406.00284 #LLMs #ATP #Prover9 #SMT #Z3

Lecturas compartidas el 30 de mayo de 2024. https://jaalonso.github.io/vestigium/posts/2024/05/31-lecturas_compartidas_el_30-may-24 #ITP #Lean4 #IsabelleHOL #Coq #Theorema #HOL_Light #Math #ATP #Prover9 #Vampire #TPTP #FunctionalProgramming #Haskell #LogicProgramming #Prolog #AI #LLMs

Prover9 unleashed: Automated configuration for enhanced proof discovery. ~ Kristina Aleksandrova, Jan Jakubuv and Cezary Kaliszyk. https://easychair.org/publications/download/tGgl #ATP #Prover9