The Linea Prover for a Very Smart High Schooler