ParentFull threadpcloadlett3r·A counterexample (at least the jacobian conjecture one) is a lot easier to manually verify than 10MB Lean proofView on HN