The simplest known single axiom for groups in terms of multiplication & inverses: ((z * (x * y)^{-1})^{-1} * (z * y^{-1})) * (y^{-1} * y)^{-1} = x (Source: K. Kunen. Single axioms for groups. J. Automated Reasoning 9 (1992), 291-308)

When Agda met Vampire. ~ Artjoms Šinkarovs, Michael Rawson. arxiv.org/abs/2602.188... #Agda #ITP #Vampire #ATP

“The amount of serendipity that will occur in your life, your Luck Surface Area, is directly proportional to the degree to which you do something you’re passionate about combined with the total number of people to whom this is effectively communicated.”

[New Blog Post] An AC Hash Cons with AC matching www.philipzucker.com/ac_hashcons/

[New Blog Post] Weighted Union Find and Ground Knuth Bendix Completion www.philipzucker.com/weighted_uf/

[New Blog Post] SMTLIB as a Compiler IR I www.philipzucker.com/smt_compiler... #compiler #smtlib

six thoughts on generating c ~~ wingolog.org/archives/202...

Proving Cauchy-Schwarz for vec3 in knuckledragger

Enjoy this free-access article from the latest issue of The Physics Teacher. doi.org/10.1119/5.02... #PhysicsTeachers #PhysicsEducation #Physics #TPT

[New Blog Post] Calling Lean Functions As Python Functions www.philipzucker.com/leancall/ #lean4 #python

[New Blog Post] Term Ordering Etudes: Ground Lexicographic Path Ordering www.philipzucker.com/lpo_etudes/ #logic

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

[New Blog Post] Subterms Modulo Theories I www.philipzucker.com/subterm_mod_... #logic

A video and notebook on a short Introduction to SMT solvers colab.research.google.com/github/philz... www.youtube.com/watch?v=cI2s...

[New Blog Post] Contextual Union Finds www.philipzucker.com/context_uf2/ #egraphs #logic

Seemingly impossible programs in Lean. ~ Joachim Breitner. www.joachim-breitner.de/blog/818-See... #ITP #LeanProver

130k lines of formal topology in two weeks: Simple and cheap autoformalization for everyone? ~ Josef Urban. arxiv.org/abs/2601.032... #ITP #Mizar #LLMs #Math #Autoformalization

Computing solutions for systems of multivariate ordinary differential equations in Rocq. ~ Holger Thies- dl.acm.org/doi/pdf/10.1... #ITP #RocqProver

Adding sorts to an Isabelle formalization of superposition. ~ Balazs Toth, Martin Desharnais-Schäfer, Jasmin Blanchette. dl.acm.org/doi/pdf/10.1... #ITP #IsabelleHOL

A lambda-superposition tactic for Isabelle/HOL. ~ Massin Guerdi. dl.acm.org/doi/pdf/10.1... #ITP #IsabelleHOL

[New Blog Post] SMTMSMT: Gluing Together CVC5 and Z3 Nelson Oppen Style www.philipzucker.com/glue-cvc5-z3/ #logic

Why did dinos eat all that plastic?

[New Blog Post] An Inequality Union Find Inspired by Atomic Asymmetric Completion www.philipzucker.com/asymmetric_c... #logic #automatedtheoremproving

[New Blog Post] Some Lean Syntax for Knuckledragger www.philipzucker.com/kd_microlean/ #logic

[New Blog Post] Semi-Interactive Assembly Verification in Knuckledragger www.philipzucker.com/asm_verify4/ #ghidra #assembly #logic #riscv #Python

A Rocq formalization of monomial and graded orders. ~ Sylvie Boldo, François Clément, Vincent Martin, Micaela Mayero. arxiv.org/abs/2512.04573 #ITP #Rocq #Math

A couple weeks ago I had the great pleasure of inviting Rustan Leino (of Dafny fame) on my podcast, to talk about all sorts of logic stuff! Part II to come soon! open.spotify.com/episode/4d9J...

[New Blog Post] SAT Etudes 2: Toy DPLL www.philipzucker.com/smt_sat_solv... #logic

[New Blog Post] Primitive, Leveled, and Quantifier Union Finds www.philipzucker.com/prim_level_uf/ #logic #egraph

Just out: Functional Data Structures, edited by Tobias Nipkow

New on my blog: Set theory with types lawrencecpaulson.github.io/2025/11/21/T...

I've pushed Knuckledragger, my z3 based python proof assistant, up to PyPI pypi.org/project/knuc...

[New Blog Post] Implementing E Unification using SMT www.philipzucker.com/smt_unify/ #logic #automatedreasoning #smt

Towards a verified compiler for Distributed PlusCal. ~ Ghilain Bergeron, Horatiu Cirstea, Stephan Merz. hal.science/hal-05329156... #ITP #LeanProver

please enjoy: my Wasm-hosted, Wasm-targeting build of Clang/Clang++/LLD: a self-contained, 25 MiB (gzipped) pure function www.npmjs.com/package/@yow...

A toy hour clock example proof in a TLA dsl of knuckledragger. Basically combinators over `Int -> T` functions. @hillelwayne.com

A gentle introduction to the axiom of choice. ~ Andreas Blass, Dhruv Kulshreshtha. arxiv.org/abs/2509.01830 #Math #SetTheory

[New Blog Post] ZF style set theory in Knuckledragger I www.philipzucker.com/zf_knuckle1/ #python #logic

A formally verified IEEE 754 floating-point implementation of interval iteration for MDPs. ~ Bram Kohlen, Maximilian Schäffeler, Mohammad Abdulaziz, Arnd Hartmanns, Peter Lammich. arxiv.org/abs/2501.10127 #ITP #IsabelleHOL

[New Blog Post] Toy Binary Decision Diagrams www.philipzucker.com/toy_bdd/ #python #logic

In honor of #racketcon I’ve bolted some quotation onto Knuckledragger github.com/philzook58/k... . Might even be sound!

Continue to feel like 95% of "why programmers should learn category theory" blogs are really "why programmers should learn abstract algebra" Which is annoying because there are 1000s of blogs on category theory and 0 on abstract algebra

Determinism types for functional logic programming. ~ Michael Hanus, Kai-Oliver Prott. www.michaelhanus.de/publications... #ITP #Rocq

Formally verifying a vertical cell decomposition algorithm. ~ Yves Bertot, Thomas Portet. drops.dagstuhl.de/storage/00li... #ITP #Rocq

[New Blog Post] Proving the Infinitude of Primes in Knuckledragger #python #logic www.philipzucker.com/knuckle_prim...

[New Blog Post] Proof Rules for MetaSMT #python #logic www.philipzucker.com/kdrag_proof_...

Case study: Verified Vampire proofs in the lambdapi-calculus modulo. ~ Anja Petković Komel, Michael Rawson, Martin Suda. arxiv.org/abs/2503.15541 #ATP #Vampire #ITP #Dedukti

Read later arxiv.org/abs/2305.15382

[New Blog Post] A Slotted Hash Cons for Alpha Invariance www.philipzucker.com/slotted_hash... #hashing #egraph #lambda

Stratified datalog and program analysis (in Isabelle/HOL). ~ Anders Schlichtkrull, René Rydhof Hansen, Flemming Nielson. www.isa-afp.org/entries/Stra... #ITP #IsabelleHOL