Why formalize mathematics – more than catching errors
rkirov.github.io
Why formalize mathematics – more than catching errors
1–10 of 80 posts
Re: Why formalize mathematics – more than catching errors
#2Much of the argument is the same as for the initial push to formalize mathematics in the late 19th century. Formalisms allow for precision and help reduce errors, but the most important change was in how mathematicians were able to communicate, by creating a shared understanding.
Computerized mathematics is just another step in that direction.
Re: Why formalize mathematics – more than catching errors
#3I've been excited about Lean for years, not because of correctness guarantees, but because it opens the door to doing maths using software development methods.
Libraries of theorems and mathematical objects, with well defined abstractions that are ergonomic to apply in target use cases. Accompanied by good documentation, focused less on how the theorems are proven (how the functions are implemented), and more on what to use them for and how. With proper version control and package management.
I believe that all these practices could vastly improve collaboration and research velocity in maths, as much or more than AI, although they are highly complementary. If maths is coding, AI will be much better at it, and AI will be more applicable to it.
Re: Why formalize mathematics – more than catching errors
#4Lean was a gamechanger for me as someone who has a "hobby" level interest in abstract mathematics. I don't have the formal education that would have cultivated the practice and repetition needed to just know on a gut level the kinds of formal manipulations needed for precise and accurate proofs. but lean (combined with its incredibly well designed abbreviation expansion) gives probably the most intuitive way to manipulate formal mathematical expressions that you could hope to achieve with a keyboard.
It provides tools for discovering relevant proofs, theorems, etc. Toying around with lean has actively taught me math that I didn't know before. The entire time it catches me any time I happen to fall into informal thinking and start making assumptions that aren't actually valid.
I don't know of any way to extract the abbreviation engine that lean plugins use in the relevant editors for use in other contexts, but man, I'd honestly love it if I could type \all or \ne to get access to all of the mathematical unicode characters trivially. Or even extend it to support other unicode characters that I might find useful to type.
Re: Why formalize mathematics – more than catching errors
#5Much of the argument is the same as for the initial push to formalize mathematics in the late 19th century. Formalisms allow for precision and help reduce errors, but the most important change was in how mathematicians were able to communicate, by creating a shared understanding. Computerized mathematics is just another step in that direction.
[deleted]
Re: Why formalize mathematics – more than catching errors
#6Lean was a gamechanger for me as someone who has a "hobby" level interest in abstract mathematics. I don't have the formal education that would have cultivated the practice and repetition needed to just know on a gut level the kinds of formal manipulations needed for precise and accurate proofs. but lean (combined with its incredibly well designed abbreviation expansion) gives probably the most intuitive way to manip…
Bessis [1] argues that formalism - or loosely math writing - is foundational to clarifying intuition/meaning in a way that natural language cannot. Imagine it as a scalpel carving out precise shapes from the blur of images we carry thereby allowing us to "see" things we otherwise cannot.
I am curious to try out lean to understand how definitions in lean are able to operationally capture meaning in an unambiguous manner.
[1] https://www.amazon.com/Mathematica-Secret-World-Intuition-Cu...
Re: Why formalize mathematics – more than catching errors
#7Lean was a gamechanger for me as someone who has a "hobby" level interest in abstract mathematics. I don't have the formal education that would have cultivated the practice and repetition needed to just know on a gut level the kinds of formal manipulations needed for precise and accurate proofs. but lean (combined with its incredibly well designed abbreviation expansion) gives probably the most intuitive way to manip…
I mean, if you understand leans system then you understand the formal manipulation needed for precise and accurate proofs. Most mathematical papers are rather handwavy about things and expect people to fill in the formalism, which is not always true, as we have seen
Re: Why formalize mathematics – more than catching errors
#8Much of the argument is the same as for the initial push to formalize mathematics in the late 19th century. Formalisms allow for precision and help reduce errors, but the most important change was in how mathematicians were able to communicate, by creating a shared understanding. Computerized mathematics is just another step in that direction.
Imho it was always "computerized", they just didn't have a computer. To me the approaches used in the early 20th century look like people defining a simple VM then writing programs that "execute" on that VM.
Re: Why formalize mathematics – more than catching errors
#9I've been excited about Lean for years, not because of correctness guarantees, but because it opens the door to doing maths using software development methods. Libraries of theorems and mathematical objects, with well defined abstractions that are ergonomic to apply in target use cases. Accompanied by good documentation, focused less on how the theorems are proven (how the functions are implemented), and more on what…
As a a hobbyist mathematician / type theorist, chatgpt et al are great at 'looking up' theorems that you want to exist but that you may not have read about yet. It's also good at connecting disparate areas of math. I don't think lean subsumes AI. Rather, lean allows you to check the AI proof. ChatGPT genuinely does have a knack for certain lines of thought.
Re: Why formalize mathematics – more than catching errors
#10I've been excited about Lean for years, not because of correctness guarantees, but because it opens the door to doing maths using software development methods. Libraries of theorems and mathematical objects, with well defined abstractions that are ergonomic to apply in target use cases. Accompanied by good documentation, focused less on how the theorems are proven (how the functions are implemented), and more on what…
Out of curiosity, does anyone know the mathematicians actively leaning into AI + Lean?