To be fair, however, these proofs are using several of the automatic proving methods built into Lean, like linarith, nlinarith, field_simp, and so on. Each of these are hundreds of lines of manually tweaked heuristics.
It's still quite interesting. I think if we had a good integration of AI methods into the Lean runtime itself the theorem prover could be excellent. You could have a cooperative model where the human mathematician writes down statements, and the AI fleshes out a proof or catches typos that you make. Right now Lean has similar functionality but the automatic proving isn't as good as it could be.
I just wish the Lean community wasn't stuck on the Lean 3 -> Lean 4 migration for the past year. I'm getting flashbacks of Python 2 -> Python 3 ....