Comment by malisper

> Given the constraint (3.5 hours of model effort) having a Lean proof is actually a sign that some of the results are likely weak

Can you explain this? How would having a lean proof of the program make it more likely the proof is weak?