Philip Zucker
@sandmouth.bsky.social
📤 300
đź“Ą 349
đź“ť 141
Computer Friend, Not a Bird www.philipzucker.com
pinned post!
I put a new preprint up summarizing a year or so of fun e-graph ideas. Check it out!
#egraphs
#logic
#compilers
arxiv.org/abs/2504.14340
loading . . .
Omelets Need Onions: E-graphs Modulo Theories via Bottom-up E-matching
E-graphs are a data structure for equational reasoning and optimization over ground terms. One of the benefits of e-graph rewriting is that it can declaratively handle useful but difficult to orient i...
https://arxiv.org/abs/2504.14340
10 months ago
0
7
1
Proving Cauchy-Schwarz for vec3 in knuckledragger
2 days ago
0
0
0
reposted by
Philip Zucker
AAPTHQ
4 days ago
Enjoy this free-access article from the latest issue of The Physics Teacher.
doi.org/10.1119/5.02...
#PhysicsTeachers
#PhysicsEducation
#Physics
#TPT
loading . . .
Orbits of Balls in a Funnel and a Spherical Surface
Many articles have been published concerning experiments with funnels and other curved surfaces to illustrate Kepler’s laws of planetary motion.1–5 The main obj
https://doi.org/10.1119/5.0229223
0
7
2
[New Blog Post] Calling Lean Functions As Python Functions
www.philipzucker.com/leancall/
#lean4
#python
loading . . .
Calling Lean Functions As Python Functions
I think Lean is neat.
https://www.philipzucker.com/leancall/
5 days ago
1
4
0
[New Blog Post] Term Ordering Etudes: Ground Lexicographic Path Ordering
www.philipzucker.com/lpo_etudes/
#logic
loading . . .
Term Ordering Etudes: Ground Lexicographic Path Ordering
Term orderings are a concept that is both obvious and bizarre.
https://www.philipzucker.com/lpo_etudes/
11 days ago
0
1
0
reposted by
Philip Zucker
José A. Alonso
13 days ago
Elementary proofs of ring commutativity theorems. ~ Michael Kinyon, Desmond MacHale.
arxiv.org/abs/2601.125...
#ATP
#Prover9
#Math
loading . . .
Elementary proofs of ring commutativity theorems
Jacobson's commutativity theorem says that a ring is commutative if, for each $x$, $x^n = x$ for some $n > 1$. Herstein's generalization says that the condition can be weakened to $x^n-x$ being centra...
https://arxiv.org/abs/2601.12599v1
0
3
1
[New Blog Post] Subterms Modulo Theories I
www.philipzucker.com/subterm_mod_...
#logic
loading . . .
Subterms Modulo Theories I
Terms are nice (trees with ordered children). They make sense You can do rewriting on them, unification (equation solving) and (unfailing) completion (equational search). They are at least a relative ...
https://www.philipzucker.com/subterm_mod_miller/
18 days ago
0
2
0
A video and notebook on a short Introduction to SMT solvers
colab.research.google.com/github/philz...
www.youtube.com/watch?v=cI2s...
loading . . .
Google Colab
https://colab.research.google.com/github/philzook58/philzook58.github.io/blob/master/pynb/2026_smt_talk_dahgstuhl_egraphs.ipynb
23 days ago
0
5
1
[New Blog Post] Contextual Union Finds
www.philipzucker.com/context_uf2/
#egraphs
#logic
loading . . .
Contextual Union Finds
Something that is desired in egraph rewriting is rewriting under assumptions.
https://www.philipzucker.com/context_uf2/
23 days ago
0
4
1
reposted by
Philip Zucker
José A. Alonso
about 1 month ago
Seemingly impossible programs in Lean. ~ Joachim Breitner.
www.joachim-breitner.de/blog/818-See...
#ITP
#LeanProver
0
2
2
reposted by
Philip Zucker
José A. Alonso
23 days ago
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
loading . . .
130k Lines of Formal Topology in Two Weeks: Simple and Cheap Autoformalization for Everyone?
This is a brief description of a project that has already autoformalized a large portion of the general topology from the Munkres textbook (which has in total 241 pages in 7 chapters and 39 sections)....
https://arxiv.org/abs/2601.03298v1
0
5
2
reposted by
Philip Zucker
José A. Alonso
23 days ago
Computing solutions for systems of multivariate ordinary differential equations in Rocq. ~ Holger Thies-
dl.acm.org/doi/pdf/10.1...
#ITP
#RocqProver
0
1
1
reposted by
Philip Zucker
José A. Alonso
23 days ago
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
0
1
1
reposted by
Philip Zucker
José A. Alonso
23 days ago
A lambda-superposition tactic for Isabelle/HOL. ~ Massin Guerdi.
dl.acm.org/doi/pdf/10.1...
#ITP
#IsabelleHOL
0
0
1
[New Blog Post] SMTMSMT: Gluing Together CVC5 and Z3 Nelson Oppen Style
www.philipzucker.com/glue-cvc5-z3/
#logic
loading . . .
SMTMSMT: Gluing Together CVC5 and Z3 Nelson Oppen Style
Satisfiability module theories solvers are a gluing together of domain specific theories with a SAT solver.
https://www.philipzucker.com/glue-cvc5-z3/
about 1 month ago
0
0
0
Why did dinos eat all that plastic?
about 1 month ago
0
0
0
[New Blog Post] An Inequality Union Find Inspired by Atomic Asymmetric Completion
www.philipzucker.com/asymmetric_c...
#logic
#automatedtheoremproving
loading . . .
An Inequality Union Find Inspired by Atomic Asymmetric Completion
Atomic asymmetric completion is a union find. Ground term asymmetric completion is a refinement egraph.
https://www.philipzucker.com/asymmetric_complete/
about 2 months ago
0
2
0
[New Blog Post] Some Lean Syntax for Knuckledragger
www.philipzucker.com/kd_microlean/
#logic
loading . . .
Some Lean Syntax for Knuckledragger
I have wired in the capability to use lean-like expression strings in places that accept formulas in knuckledragger https://github.com/philzook58/knuckledragger .
https://www.philipzucker.com/kd_microlean/
about 2 months ago
0
2
0
[New Blog Post] Semi-Interactive Assembly Verification in Knuckledragger
www.philipzucker.com/asm_verify4/
#ghidra
#assembly
#logic
#riscv
#Python
loading . . .
Semi-Interactive Assembly Verification in Knuckledragger
I’ve been working on an interactive proof experience in python for assembly code.
https://www.philipzucker.com/asm_verify4/
about 2 months ago
0
1
0
reposted by
Philip Zucker
José A. Alonso
2 months ago
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
loading . . .
A Rocq Formalization of Monomial and Graded Orders
Even if binary relations and orders are a common formalization topic, we need to formalize specific orders (namely monomial and graded) in the process of formalizing in Rocq the finite element method....
https://arxiv.org/abs/2512.04573
0
0
1
reposted by
Philip Zucker
Cody
2 months ago
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...
loading . . .
Rustan Leino - part I
Spotify video
https://open.spotify.com/episode/4d9JYwNPV1Sw5hOYcZS1sp?si=jQnIuHuQQeOJ2bv5wz6GMw
1
8
4
[New Blog Post] SAT Etudes 2: Toy DPLL
www.philipzucker.com/smt_sat_solv...
#logic
loading . . .
SAT Etudes 2: Toy DPLL
Another post about SAT solvers, probably heading towards SMT solvers.
https://www.philipzucker.com/smt_sat_solver2/
2 months ago
0
4
0
[New Blog Post] Primitive, Leveled, and Quantifier Union Finds
www.philipzucker.com/prim_level_uf/
#logic
#egraph
loading . . .
Primitive, Leveled, and Quantifier Union Finds
There is an interesting and simple union find variation that allows primitives into the union find.
https://www.philipzucker.com/prim_level_uf/
2 months ago
0
5
3
reposted by
Philip Zucker
Lawrence Paulson
2 months ago
Just out: Functional Data Structures, edited by Tobias Nipkow
0
25
11
reposted by
Philip Zucker
Lawrence Paulson
3 months ago
New on my blog: Set theory with types
lawrencecpaulson.github.io/2025/11/21/T...
loading . . .
Set theory with types
https://lawrencecpaulson.github.io/2025/11/21/Typed_Set_Theory.html
1
3
2
I've pushed Knuckledragger, my z3 based python proof assistant, up to PyPI
pypi.org/project/knuc...
loading . . .
knuckledragger
Interactive Theorem Prover
https://pypi.org/project/knuckledragger/
3 months ago
1
9
1
[New Blog Post] Implementing E Unification using SMT
www.philipzucker.com/smt_unify/
#logic
#automatedreasoning
#smt
loading . . .
Implementing E Unification using SMT
Unification is a logical flavored word for the notion of equation solving.
https://www.philipzucker.com/smt_unify/
3 months ago
0
2
0
reposted by
Philip Zucker
José A. Alonso
3 months ago
Towards a verified compiler for Distributed PlusCal. ~ Ghilain Bergeron, Horatiu Cirstea, Stephan Merz.
hal.science/hal-05329156...
#ITP
#LeanProver
0
2
1
reposted by
Philip Zucker
Catherine
3 months ago
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...
loading . . .
4
155
33
A toy hour clock example proof in a TLA dsl of knuckledragger. Basically combinators over `Int -> T` functions.
@hillelwayne.com
4 months ago
0
1
0
reposted by
Philip Zucker
José A. Alonso
4 months ago
A gentle introduction to the axiom of choice. ~ Andreas Blass, Dhruv Kulshreshtha.
arxiv.org/abs/2509.01830
#Math
#SetTheory
loading . . .
A Gentle Introduction to the Axiom of Choice
This article offers a gentle introduction to the axiom of choice. We introduce the axiom, discuss some common objections to it, and present three kinds of reasons to accept it. Although the exposition...
https://arxiv.org/abs/2509.01830
0
4
2
[New Blog Post] ZF style set theory in Knuckledragger I
www.philipzucker.com/zf_knuckle1/
#python
#logic
loading . . .
ZF style set theory in Knuckledragger I
Zermelo-Fraenkel set theory is a theory of sets.
https://www.philipzucker.com/zf_knuckle1/
4 months ago
0
0
0
reposted by
Philip Zucker
José A. Alonso
4 months ago
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
loading . . .
A Formally Verified IEEE 754 Floating-Point Implementation of Interval Iteration for MDPs
We present an efficiently executable, formally verified implementation of interval iteration for MDPs. Our correctness proofs span the entire development from the high-level abstract semantics of MDPs...
https://arxiv.org/abs/2501.10127
0
1
1
[New Blog Post] Toy Binary Decision Diagrams
www.philipzucker.com/toy_bdd/
#python
#logic
loading . . .
Toy Binary Decision Diagrams
Binary decision diagrams https://en.wikipedia.org/wiki/Binary_decision_diagram are a data structure for storing boolean functions, spiritually something like [Bool] -> Bool. You can tabulate such a th...
https://www.philipzucker.com/toy_bdd/
4 months ago
0
0
0
In honor of
#racketcon
I’ve bolted some quotation onto Knuckledragger
github.com/philzook58/k...
. Might even be sound!
loading . . .
knuckledragger/src/kdrag/theories/sexp.py at main · philzook58/knuckledragger
A Low Barrier Proof Assistant. Contribute to philzook58/knuckledragger development by creating an account on GitHub.
https://github.com/philzook58/knuckledragger/blob/main/src/kdrag/theories/sexp.py
4 months ago
0
0
0
reposted by
Philip Zucker
Hillel
4 months ago
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
6
68
1
reposted by
Philip Zucker
José A. Alonso
4 months ago
Determinism types for functional logic programming. ~ Michael Hanus, Kai-Oliver Prott.
www.michaelhanus.de/publications...
#ITP
#Rocq
0
0
1
reposted by
Philip Zucker
José A. Alonso
4 months ago
Formally verifying a vertical cell decomposition algorithm. ~ Yves Bertot, Thomas Portet.
drops.dagstuhl.de/storage/00li...
#ITP
#Rocq
0
0
1
[New Blog Post] Proving the Infinitude of Primes in Knuckledragger
#python
#logic
www.philipzucker.com/knuckle_prim...
loading . . .
Proving the Infinitude of Primes in Knuckledragger
Cody challenged me to prove that there are an infinitely many primes in Knuckledragger, saying it’s the minimum thing to do to demonstrate you have a proof assistant. https://en.wikipedia.org/wiki/Euc...
https://www.philipzucker.com/knuckle_primes/
4 months ago
0
3
1
[New Blog Post] Proof Rules for MetaSMT
#python
#logic
www.philipzucker.com/kdrag_proof_...
loading . . .
Proof Rules for MetaSMT
Knuckledragger https://github.com/philzook58/knuckledragger is my system for interactive theorem proving in python. The core system is not python specific and has some interesting theoretical aspects.
https://www.philipzucker.com/kdrag_proof_rules/
5 months ago
0
3
0
reposted by
Philip Zucker
José A. Alonso
5 months ago
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
loading . . .
Case Study: Verified Vampire Proofs in the LambdaPi-calculus Modulo
The Vampire automated theorem prover is extended to output machine-checkable proofs in the Dedukti concrete syntax for the LambdaPi-calculus modulo. This significantly reduces the trusted computing ba...
https://arxiv.org/abs/2503.15541
0
5
1
reposted by
Philip Zucker
Alex Nelson
5 months ago
Read later
arxiv.org/abs/2305.15382
loading . . .
Theorem Proving in Dependently-Typed Higher-Order Logic -- Extended Preprint
Higher-order logic HOL offers a very simple syntax and semantics for representing and reasoning about typed data structures. But its type system lacks advanced features where types may depend on terms...
https://arxiv.org/abs/2305.15382
0
1
1
[New Blog Post] A Slotted Hash Cons for Alpha Invariance
www.philipzucker.com/slotted_hash...
#hashing
#egraph
#lambda
loading . . .
A Slotted Hash Cons for Alpha Invariance
Slotted e-graphs https://dl.acm.org/doi/10.1145/3729326 are a data structure that compactly stores many equivalent terms in an alpha invariant aware way. I’ve been very excited by them but also very c...
https://www.philipzucker.com/slotted_hash_cons/
5 months ago
0
2
0
reposted by
Philip Zucker
José A. Alonso
5 months ago
Stratified datalog and program analysis (in Isabelle/HOL). ~ Anders Schlichtkrull, René Rydhof Hansen, Flemming Nielson.
www.isa-afp.org/entries/Stra...
#ITP
#IsabelleHOL
loading . . .
Stratified Datalog and Program Analysis
Stratified Datalog and Program Analysis in the Archive of Formal Proofs
https://www.isa-afp.org/entries/Stratified_Datalog.html
0
2
1
reposted by
Philip Zucker
Michael Goerz
5 months ago
A quick note on Lindblad operators in composite systems. Something I've been confused about for years.
#quantum
goerz-research.github.io/2025-09-11_C...
Also contains a useful
#JuliaLang
implementation for a partial trace function, if you ever need that (surprisingly tricky!)
loading . . .
https://goerz-research.github.io/2025-09-11_Composite_Dissipation/CompositeDissipation.html
0
6
1
reposted by
Philip Zucker
Cody
5 months ago
I'm actually kind of proud of this one:
open.spotify.com/episode/6LNn...
loading . . .
TREE(3) and the Kruskal theorem
Spotify video
https://open.spotify.com/episode/6LNnPGh3pKlc4qQHfzTnmi?si=24ec7dd082004664
1
1
1
[New Blog Post] Compositional Datalog on SQL: Relational Algebra of the Environment
#datalog
#database
#sql
www.philipzucker.com/compose_data...
loading . . .
Compositional Datalog on SQL: Relational Algebra of the Environment
I spent sone time making Datalogs that translated into SQL. https://www.philipzucker.com/tiny-sqlite-datalog/
https://www.philipzucker.com/compose_datalog/
5 months ago
0
6
1
[New Blog Post] A Python CLI for Verifying Assembly
#formalmethods
#assembly
#compilers
www.philipzucker.com/asm_verify3/
loading . . .
A Python CLI for Verifying Assembly
I’ve been building a system that verifies assembly programs via symbolic execution. I think the following are the most novel points of my approach:
https://www.philipzucker.com/asm_verify3/
6 months ago
0
2
1
reposted by
Philip Zucker
José A. Alonso
6 months ago
The Vampire diary ~ Filip Bártek et als.
arxiv.org/abs/2506.03030
#ATP
#Vampire
loading . . .
The Vampire Diary
During the past decade of continuous development, the theorem prover Vampire has become an automated solver for the combined theories of commonly-used data structures. Vampire now supports arithmetic,...
https://arxiv.org/abs/2506.03030
0
1
1
reposted by
Philip Zucker
José A. Alonso
6 months ago
Second analysis lecture "Filter" (June 17, 2025). ~ Alex Kontorovich.
alexkontorovich.github.io/2025SimonsFo...
#ITP
#LeanProver
#Math
0
2
1
[New Blog Post] Knuckledragger Analysis Etudes
www.philipzucker.com/knuckle_anal...
loading . . .
Knuckledragger Analysis Etudes
I got kind of discouraged maybe 6 months ago trying some real analysis stuff.
https://www.philipzucker.com/knuckle_analysis1/
6 months ago
0
1
0
Load more
feeds!
log in
