For people not familiar with the subject (or Buzzard and his cohort) I recommend checking out the Zulip archive https://leanprover-community.github.io/archive/1

For people not familiar with the subject (or Buzzard and his cohort) I recommend checking out the Zulip archive https://leanprover-community.github.io/archive/116395maths/index.html https://leanprover-community.github.io/archive/116395maths/i... Some of the (esp. earlier) threads are very illuminating on the process of constructing proofs using ITPs (interactive theorem provers). My personal experience is that modeling a suitable domain of math formally can be a very good pedagogical exercise. There are many fine points that are easy to ignore when doing math informally but a formal tool would not let you. This is particularly helpful when working on foundational subjects. When successful you are rewarded with the feeling of possessing the understanding at a level deeper than everyone else (most likely untrue, but certainly a typical expository paper or book could not cover the subject as thoroughly). That said note my use of the word "modeling". In a formalization attempt you may have in your head an isomorphism between the code and the mathematical objects under study but the isomorphism is not necessarily apparent or universally recognized. Beyond the most quotidian matters other people's modeling code (think of it as an API) may or may not fit with your conceptual models. Just like there are different programming languages and libraries, there is no universally accepted approach to encode mathematical constructs. Your claim of correctness is only as good as your axioms and definitions. Your theorem, with all definitions completely unfolded, will be an unreadable tangle of first order logic formulas that anyone would be hard pressed to recognize as universally meaningful -- though it is extremely likely to be logically sound. Even if no one questions the soundness of your logic there is no tool that can certify that your formal expression actually means what you say it means in a mathematical domain.