A new blog post, Arenas, Cyclic Terms, and Flat Equational Systems www.philipzucker.com/arena_coegra... #datastructures

A New Blog Post: Lifting E-Graphs www.philipzucker.com/lifting_egra... #egraphs

Z3! You're on WATCH! Latest update to lean.py is a drop in replacement for Z3! Everyone's trying to put SMT solvers in their theorem prover, how about putting a theorem prover in your SMT solver? and here's the crazy thing: One click install, if you know Z3, you KNOW lean.py. You are not ready.

Four–in-a-row in Rocq. ~ Laurent Théry. inria.hal.science/hal-05625464... #RocqProver #ITP

Craziest thing about lean.py? You can roll your own (almost) feature-parity successor to Dafny. Python programs. Lean obligations. Grind as a solver. Proof complete. Program verified. Python code. Real.

Interesting, someone is reviving prover9 github.com/AlgorithmicT...

[New Blog Post] Reading Proof Objects and Completed Rewrite Systems from eprover into Knuckledragger www.philipzucker.com/proof_proces... #python #logic #automatedtheoremproving #formalmethods

Pretty interesting experiment in rust bindings to vampire docs.rs/vampire-prov... I feel like this is an uphill maintenance battle though

Verified tableaux: from modal logics to modal fixpoint logics. link.springer.com/article/10.1... #CoqProver #ITP #Logic

[New Blog Post] Family Orienting Python Frozenset Dependent Type Theory www.philipzucker.com/dtt_python_f... #logic #python #typetheory

scheme-rs 0.2 has been released! Lots of new features but my favorite is the params system which allows you to share rust mutable variables over a scheme delimited continuation. This solves the “how do I share this mutable reference with my scripting language” problem github.com/maplant/sche...

New on my blog: Mizar: the first usable proof assistant for mathematics lawrencecpaulson.github.io/2026/05/07/M...

ML researchers know Python. Proof engineers know Lean. Never the two should meet.. Until now! Announcing Lean.py, effortless Lean to Python and Python to Lean bindings! - Write Lean tactics in Python - Access the Python ecosystem in Lean github.com/kiranandcode...

Announcing: Myo, the LCF-style proof assistant based on Intuitionistic first-order logic plus Feferman's FS0 set theory. It's very coarse, literally the first public commit and nothing more. But it's quite capable. codeberg.org/pqnelson/myo

[New Blog Post] Lifting and Lowering Functions with The Dump Calculus www.philipzucker.com/dump_calculus/ #python #functionalprogramming #logic #egraphs

Tries for Polynomials doisinkidney.com/posts/2026-0...

People on the internet (👋 @bartoszmilewski.bsky.social, @sjoerdvisscher.w3future.com) made my mind drift toward proarrow equipments today. I never really paid attention before. It's a quite minimalistic, but natural setting. 1/5

Otten and Kreitz's "T-String-Unification: Unifying Prefixes in Non-Classical Proof Methods" seems like a suitable proxy, though... (Well, I hope, because I don't have access to Wallen's book, so I cannot say if it is adequate or not as a substitute.)

Thinning/Lifting E-Graphs for Alpha Equivalence: Checkpoint I www.philipzucker.com/thin_egraph/ #rust #egraphs

Hi! We build fast verilog simulators using just in time compilation. Our simulator outperforms existing verilog simulators by up to x100. verijit is a project by @cfbolz.bsky.social and Can Joshua Lehmann. Check out out demo video here: www. youtube.com/watch?v=PXgUsEjvAOY

Finally proved the critical pair lemma in Lean! Not sure if it's been done before (in Lean, it's been done in Isabelle and Coq both, I believe). github.com/codyroux/tra... I prematurely announced this, but I hadn't quite proven the full theorem yet...

Ayooo??? new blog post??? already???? kirancodes.me/posts/log-wh...

My blog had evolved into an unfriendly wall of links. To fix this I added an on-ramp section at the beginning. brandonrohrer.org

So. I did a thing. This was actually quite a lot of work, so I'm quite proud of this one. I wrote a tiny example of a sheaf interpreter (in Haskell). github.com/aspiwack/she... 1/8

EGRAPHS Workshop deadline in two weeks (Apr 17)! Plenty of time to whip up your presentation proposal. Remote/in-person, in-progress or already published work is welcome.

[New Blog Post] Alpha Equivalent Hash Consing with Thinnings www.philipzucker.com/thin_hash_co... #logic #datastructure

☕️ LATTE, our little workshop on hardware design languages/compilers/etc., has 24 (!) rad-looking position papers this year. It’s on Monday, and you can attend on Zoom or in Pittsburgh: https://capra.cs.cornell.edu/latte26/

A little taste of refinement python

Awesome! There was a pyiodide build but it stalled out github.com/Z3Prover/z3/... is this a different approach?

A formalization of abstract rewriting in Agda. ~ Sam Arkle, Andrew Polonsky. arxiv.org/abs/2603.109... #Agda

[New Blog Post] Monus, Factor, and Thinning Union Finds www.philipzucker.com/thin_monus_uf/ #python #math #logic

Feferman's FS0 is built atop *classical* first-order logic with equality. Do we gain anything by restricting ourselves to *Intuitionistic* first-order logic with equality? I mean, besides a headache...

Refinement Modeling and Verification of RISC-V Assembly using Knuckledragger www.philipzucker.com/refine_assem... #assembly #riscv #formalmethods #python with video www.youtube.com/watch?v=NQGh...

[New Blog Post] Thinnings: Sublist Witnesses and de Bruijn Index Shift Clumping www.philipzucker.com/thin1/ #python #logic #math

[New Blog Post] State of Knuckledragger III: Kernel Changes, Symbolic Union, AI, and more www.philipzucker.com/state_o_knuc... #python #logic #theoremproving

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...