by John on (#767R2)
I ran an experiment today to see whether Claude [1] could generate Lean code to prove a calculation at the bottom of this post, six lines of calculus. I started with this prompt This page contains a mathematical proof that a Fourier coefficient, a_n, is given in terms of a Bessel function. The LaTeX source [...]The post Formally proving a calculation with Claude and Lean first appeared on John D. Cook.