Tags

Tags are free keywords, one index page, no page per tag. The blog's three subjects — formal verification, mathematics, tooling — are categories instead, and each of those has its own page under Categories.

Agda

• Quotients without quotient types
• Building the Agda MCP: field notes
• The typechecker as a reward signal

Coq

• Diaconescu's Theorem

GAP

• Overalgebras

Lean

• OpenAI and the finite lattice representation problem

MCP

• Building the Agda MCP: field notes

SAT

• 3-SAT and Partition Lattices

UACalc

• Overalgebras

agda-mcp

• Building the Agda MCP: field notes

axiom of choice

• Diaconescu's Theorem

complexity

• 3-SAT and Partition Lattices

congruence lattices

• A Problem of Pálfy and Saxl
• IEProps
• Isotopy
• Overalgebras
• OpenAI and the finite lattice representation problem

constructive mathematics

• Diaconescu's Theorem
• Quotients without quotient types

evaluation

• The typechecker as a reward signal

finite groups

• GroupSound
• IEProps
• OpenAI and the finite lattice representation problem

harmonic analysis

• GroupSound

isotopy

• Isotopy

language models

• Building the Agda MCP: field notes
• The typechecker as a reward signal
• OpenAI and the finite lattice representation problem

lattice theory

• 3-SAT and Partition Lattices
• Congruences of Partial Algebras

open problems

• A Problem of Pálfy and Saxl
• OpenAI and the finite lattice representation problem

proof search

• The typechecker as a reward signal

setoids

• Quotients without quotient types

signal processing

• GroupSound

universal algebra

• A Problem of Pálfy and Saxl
• IEProps
• Isotopy
• Overalgebras
• Congruences of Partial Algebras
• Quotients without quotient types
• OpenAI and the finite lattice representation problem