Comment by jeremyjh

I will not be surprised if the number is zero. It should have already happened if it were possible.

Proving that a conjecture is false is very different than what you are proposing. You are proposing an existing proof is simply wrong, that the proof can be checked in Lean, and that no one has bothered to check it yet.