Definition
Plain language
A statement accepted as true without proof, used as a starting assumption.
As stated in the literature
An unproven proposition admitted into a formal system; injecting spurious axioms is a way agents pass the proof-assistant kernel without actually proving the target theorem.
Also called: axioms
Why it matters: Axioms are the foundation everything else rests on, so a sneaky false one can let a system 'prove' things that aren't actually true.
For example, 'two points determine exactly one line' is accepted as a starting truth from which other geometry facts are proven.
Heard on the show
“Every Lean proof ultimately rests on a tiny set of built-in foundational axioms in the kernel.”Episode 188 — A Coding Agent Found a Hole in a Peer-Reviewed STOC Proof for Five Dollars