I’ve been working on Knuckledragger, my Z3 based semi-automated python proof assistant, on and off for 6 months (or arguably five years). I’ve realized I’ve done a bunch of stuff and despite writing often, not written the slightest bit about much of it.| Hey There Buddo!
A classical theorem is that $\sqrt{2}$ is irrational. https://en.wikipedia.org/wiki/Square_root_of_2#Proofs_of_irrationality This means it cannot be written as $\frac{p}{q}$ for integers $p$ and $q$.| Hey There Buddo!