Actually, I have been diving into some specific topics lately, and simultaneously formalizing the theorems in Lean to help with understanding. The amount of omissions and handwaving going on in “proofs” in textbooks is insane. (To the point where I am not smart enough to figure out how to fill in some omissions.)
And I know that textbooks often only present a summary of a proof, and cite a more detailed source. But sometimes there is no citation at all, and even in cases where a citation exists, it might not contain the missing details.
seems like you can get this in pure math between conflicting formal systems
Hm… I don’t feel like this is what’s happening in most cases I encounter? Once I have a detailed pen-and-paper set-theoretic proof, it’s mostly straightforward to translate that to Lean’s type theory.
Actually, I have been diving into some specific topics lately, and simultaneously formalizing the theorems in Lean to help with understanding. The amount of omissions and handwaving going on in “proofs” in textbooks is insane. (To the point where I am not smart enough to figure out how to fill in some omissions.)
And I know that textbooks often only present a summary of a proof, and cite a more detailed source. But sometimes there is no citation at all, and even in cases where a citation exists, it might not contain the missing details.
Hm… I don’t feel like this is what’s happening in most cases I encounter? Once I have a detailed pen-and-paper set-theoretic proof, it’s mostly straightforward to translate that to Lean’s type theory.