A good way to do this is to replace Geometry class. It is only there because Euclid’s Elements was read by Charlemagne’s kids. Geometry teaches proof, but a

A good way to do this is to replace Geometry class. It is only there because Euclid’s Elements was read by Charlemagne’s kids. Geometry teaches proof, but a very outdated style of proof. It should be replaced with formal proofs, written in Lean or Coq. Since “a proof is a program”, it would also introduce programming into the curriculum.