{'fraction_non_alphanumeric': 0.023809523809523808, 'fraction_numerical': 0.0, 'mean_word_length': 5.582608695652174, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Mechanising Hilbert's Foundations of Geometry in Isabelle

This project continues and revises Meikle’s mechanisation of Hilbert’s Foundations of Geometry in Isabelle/HOL, focusing on declarative-style proofs to create readable and maintainable proof documents. In the interests of readability and conciseness, we have investigated general-purpose abstractions for geometric reasoning, and have shown how these can simplify existing proofs. We have revised many of the existing definitions by introducing new types, and analysed the notion of rays and half-planes more deeply than Hilbert had originally. Finally, we have corrected subtle mistakes in Meikle’s mechanised axioms of Group III, forcing us to produce new corrected proofs of the early theorems.