Formally proving a calculation with Claude and Lean (opens in new tab)

I ran an experiment today to see whether Claude 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 for […] The post first appeared on .