Comment by hgsgm

The ABC conjecture "proof" is rejected because it uses definitions and arguments no one understands.

It would not necessarily be hard to program in those incoherent definitions and get them to prove a result. That wouldn't mean much.

This is different from just programming in the conjecture and letting Lean find a complete proof.