Coq · Interactive demo
Circle-Polygon Overlap
The exact area where a circle and a polygon overlap, found by sweeping a signed area along the boundary. Comes with an interactive demo and a Coq proof of the square-and-circle case.
Maths
Proofs
Proofs and investigations, many of them machine-checked in Coq. Each one links to its source on GitHub.
Write-up
A Complex Equation Envelope
Written up as a PDF, with a Pygame script on GitHub for exploring the idea interactively.
Coq
Bird-Meertens Maximum Segment Sum
Translating a theorem from the Bird-Meertens formalism into Coq: the maximum segment sum, the problem Kadane's algorithm solves.
Coq
Zeckendorf's Theorem
An attempt to prove Zeckendorf's theorem in Coq without looking it up, as a personal challenge.
Investigation
Lerp Reverse Maths
Working out which assumptions are enough to derive the ubiquitous lerp function and its properties.
Proof
Odd and Even Parts
Recreating a simple proof that every function between fields splits into the sum of an even and an odd function.
Proof
The MU Puzzle
A proof that Douglas Hofstadter's MU puzzle, from Gödel, Escher, Bach, has no solution.
Category theory
Free Monoid
Learning about free objects in category theory, with Bartosz Milewski's Category Theory for Programmers as a guide.
Coq · Work in progress
Superposition Principle
An investigation into the superposition principle for differential equations.
The ballot box picture on Vote Share is from Wikimedia Commons, licensed under the Creative Commons Attribution-ShareAlike 3.0 License and the GNU Free Documentation License, version 1.2 or later.