Post #4445802
2026-07-21 17:39 UTC
@mjd@mathstodon.xyz do you actually need to check all the imported definitions? Or just the ones used in the headline theorem?
Replies (2)
-
@pozorvlak@mathstodon.xyz 2026-07-21 17:45
@mjd@mathstodon.xyz if the headline theorem talks about foozles and the mathlib definition of a foozle is wrong, then you've proved the wrong theorem. But the incorrect definition of foozle is only used in some intermediate lemmas, and is used consistently, then you have a correct overall proof.
-
@roboguy@mathstodon.xyz 2026-07-21 17:53
@pozorvlak@mathstodon.xyz @mjd@mathstodon.xyz That is not necessarily so easy. It might take a lot of machinery just to state the main theorem.