Lightnews — Scholar-powered news

A Gentle Introduction to the Axiom of Choice

1 5

Reposted by Philip Zucker

José A. Alonso @jalonso.bsky.social · 11h

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

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

ZF style set theory in Knuckledragger I

2 4

Philip Zucker @sandmouth.bsky.social · 1d

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

Zermelo-Fraenkel set theory is a theory of sets.

Zermelo Fraenkel Set Theory in Higher-Order Logic

Philip Zucker @sandmouth.bsky.social · 5d

My main touchstones are reading Halmos and www.isa-afp.org/entries/ZFC_... . I know set theory goes light years beyond this stuff, but this is where I'm at

Zermelo Fraenkel Set Theory in Higher-Order Logic in the Archive of Formal Proofs

www.isa-afp.org

knuckledragger/src/kdrag/theories/logic/zf.py at main · philzook58/knuckledragger

Philip Zucker @sandmouth.bsky.social · 5d

Mizar is an fascinating seeming system. I'm intrigued at the idea of developing some zf github.com/philzook58/k... My main approach has been to just wing it. In previous iterations I haven't even gotten past the basic axioms before my attention span wanders.

A Low Barrier Proof Assistant. Contribute to philzook58/knuckledragger development by creating an account on GitHub.

github.com

A Formally Verified IEEE 754 Floating-Point Implementation of Interval Iteration for MDPs

Reposted by Philip Zucker

José A. Alonso @jalonso.bsky.social · 7d

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

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

Toy Binary Decision Diagrams

Philip Zucker @sandmouth.bsky.social · 7d

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

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

knuckledragger/src/kdrag/theories/sexp.py at main · philzook58/knuckledragger

Philip Zucker @sandmouth.bsky.social · 10d

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

A Low Barrier Proof Assistant. Contribute to philzook58/knuckledragger development by creating an account on GitHub.

github.com

Reposted by Philip Zucker

Hillelogram @hillelwayne.com · 13d

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 1 68

Reposted by Philip Zucker

José A. Alonso @jalonso.bsky.social · 15d

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

Reposted by Philip Zucker

José A. Alonso @jalonso.bsky.social · 16d

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

Philip Zucker @sandmouth.bsky.social · 15d

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

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

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.

1 2

Philip Zucker @sandmouth.bsky.social · 21d

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

Proof Rules for MetaSMT

Case Study: Verified Vampire Proofs in the LambdaPi-calculus Modulo

Reposted by Philip Zucker

José A. Alonso @jalonso.bsky.social · 26d

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

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

Theorem Proving in Dependently-Typed Higher-Order Logic -- Extended Preprint

1 5

Reposted by Philip Zucker

Alex Nelson @pqnelson.bsky.social · 28d

Read later

arxiv.org/abs/2305.15382

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

A Slotted Hash Cons for Alpha Invariance

Philip Zucker @sandmouth.bsky.social · 29d

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

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