"Momentary reward to find flaw" is a hallmark crankpot tell. Fwiw, frontier labs are burning $$$$ on armies of agents trying to find contradictions, because it's much easier than constructing a proof. So, your "make Lean proof for $Millennium_Prize_Problem_X" afternoon session is certainly bogus.