Tamás Hausel · Institute of Science and Technology Austria
almanacA0a · every result, one row each, joined across the three layers
This is a complete record of one small mathematical result
in three layers — an informal proof, a computer program, and a machine-checked formal proof
— together with a per-claim account of what actually warrants each one.
results carry a proof-kernel certificate. Of the rest, 1 rests on a
refereed written argument and 2 on computation over a stated range — three different
kinds of check, kept visibly different, and always named in that order: ink, orange, blue.
Results recorded
12
one row each, joined across three layers
Refereed argument
1
read adversarially, recorded per row
Computed over a range
2
the bound is part of the claim
Kernel-certified
9
axioms measured, no gaps admitted
Peer review to date
Internal
external refereeing is a step still ahead
Human minutes
0
in the assembly itself
Machine minutes
205
wall clock, one session
Three kinds of check. A proof kernel checking a proof, a program
checking ten thousand cases, and a referee reading an argument are not the same evidence, and
this almanac never lets them blur into “we showed”. Every result below states which one it has — and a
kernel certifies the formal statement. Whether that statement is faithful to the informal
one can be decided from the warrants and the convention frame carried on every row.