Would any #LeanProver people be able to talk to me about the similarities between "simplification" of mathematical expressions, and type-theoretic proofs?
Like, a common task in computer algebra is to automatically rewrite expressions to a "simpler" form. Ideally, you'd have a proof that the simplified expression is equivalent to the original. Could this sort of thing fall out of Lean naturally?
It's the second and last day of the Lean for the Curious Mathematician colloquium in Düsseldorf already! Kaiyu Yang is explaining Theorem Proving via Machine Learning to us on a mathematician(and compiler engineer)-friendly level #leanprover#lftcm