TL;DR
This paper formalizes a problem from the 52nd International Mathematical Olympiad within the framework of ordered regular incidence planes, providing a rigorous geometric proof of its validity in this setting.
Contribution
It introduces a formal axiomatic approach to a well-known Olympiad problem, extending its validity to ordered regular incidence planes.
Findings
The problem is valid in ordered regular incidence planes.
Ordered regular incidence planes can be embedded in projective ordered planes.
A formal proof of the Olympiad problem within this geometric framework.
Abstract
We present the problem stated in intuitive language as problem 2 at the 52nd International Mathematical Olympiad as a formal statement, and prove that it is valid in ordered regular incidence planes, the weakest ordered geometry whose models can be embedded in projective ordered planes.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.