Output details
11 - Computer Science and Informatics
University of Edinburgh
An Investigation of Hilbert's Implicit Reasoning through Proof Discovery in Idle-Time
<11> Originality: This is the first extensive mechanisation of Hilbert's Foundations of Geometry that aims to capture the proofs faithfully by matching their prose-like nature.
Significance: This research, aside from pushing the boundaries of formalized mathematics, provides a formal investigation by computer of a famous piece of work, which is both mathematically and historically important. It provides clear evidence that proof assistants, with the right expertise, can act as valuable tools for informed studies on mathematicians and their work.
Rigour: The reasoning is fully mechanized in the HOL Light theorem prover, thereby guaranteeing its correctness.