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¶
GAP¶
Lean¶
MCP¶
SAT¶
UACalc¶
agda-mcp¶
axiom of choice¶
clone theory¶
complexity¶
computational complexity¶
congruence lattices¶
- A Problem of Pálfy and Saxl
- IEProps
- Isotopy
- Overalgebras
- OpenAI and the finite lattice representation problem
constraint satisfaction¶
constructive mathematics¶
evaluation¶
finite groups¶
harmonic analysis¶
isotopy¶
language models¶
- Building the Agda MCP: field notes
- The typechecker as a reward signal
- OpenAI and the finite lattice representation problem
- The ETH refutation and its impact
lattice theory¶
open problems¶
- A Problem of Pálfy and Saxl
- OpenAI and the finite lattice representation problem
- The ETH refutation and its impact