6 ms·
About 8 to 9 years ago I asked Michael Nielsen (one of the authors of this PDF) by email what he thinks about interactive theorem proving. He was kind enough to
by practal 4y ago
About 8 to 9 years ago I asked Michael Nielsen (one of the authors of this PDF) by email what he thinks about interactive theorem proving. He was kind enough to answer, and replied something along the lines of that he doesn't believe mechanised logic will change how mathematicians work (if I remember correctly).
I think interactive theorem proving (ITP) is the ultimate tool of thought, though.
Although as a field it exists for quite some time, I think it is only now starting to show its full potential, as everybody starts to realise what powerful AI can do for ITP automation. Things like Mathematica and AutoCad should really be just special apps running on top of an ITP operating system.
- haskellandchill 4y agohey no offense but right now you're giving off big crank energy. no one is going to take your "abstraction logic" seriously because it's disconnected from the literature and completely unverified. your characterization of things is strange, there is no Rasiowa’s approach that missed a generalization that a modern presentation of Frege's work shows. it's hard to understand from a glance what you are calling "abstraction logic" is but it's near certain it's already been classified as something in the literature. if not then write up a basic result properly so someone in the field can tell you have something at a glance and publish your result with them, you can be first author so it's not like you're giving up any glory and they will ensure you are peer reviewed through the right channels. but you most likely have no result to speak off. which is fine. just build something. we need more ITPs in the wild, and currently have more of a UI and OS problem than a lack of proper theory.
- mbrodersen 4y agoI agree. Learning how to use interactive theorem proving tools like Coq, LEAN etc. has blown my mind and given me a much better way to think about software development. The same way that learning basic maths teaches you a new way to think clearly about the messy real world.
- pizza 4y agoHow did you do approach learning it to make it “stick” to such an extent that it’s changed how you approach problems?
- mbrodersen 4y agoI completed the first volume of Software Foundations: https://softwarefoundations.cis.upenn.edu/ https://softwarefoundations.cis.upenn.edu/ and then started proving tiny toy examples correct from scratch. I also read a lot of papers on type theory and the history of proof assistants. It’s really interesting fun stuff.
- closedloop129 4y agoITP is a key part and a good start but I wouldn't call it the ultimate tool. Thought is more than logic. Logic operates on a model, after things have been named and conceptualized. As the saying goes, there are two hard things in computer science, and ITP doesn't cover all of them.
- practal 4y agoI would say it covers naming things and cache invalidation. And it is really really good at avoiding off-by-one errors.
- jolux 4y agohow does it cover naming things?
- practal 4y agoThat depends on the ITP system. But in general, in an ITP system you can separate the name of something from how it is displayed. In the ITP system I am currently building, Practal, the displayed syntax does not need to be unique. So choosing a unique name becomes simpler, because you don't have to worry so much about how it looks, because that can be entirely different and doesn't need to be unique. Apart from that, every accessible element of your mathematical universe already has a name: it is the term you use to describe it.
- beckingz 4y agoSure you can rename things easily, but NAMING something CORRECTLY is hard, in an ontological sense where you may not know what the thing's name is until you truly know what it is.
- jolux 4y agoI've never thought that "naming things" meant keeping track of the name or anything, but that's hard too. I've always thought it meant the descriptive aspect of naming.
- Nokinside 4y agoMathematics is the most creative work there is, so if you can automate the tedious work, it helps, but no miracles. Theorem proving requires unnecessarily formal reasoning chain that is usually more work than worth. The way most mathematicians work is: First they figure out what the lemma or theorem they want is. Then they try to prove it. I think theorem proofing will be beneficial for programmers and inside a compiler. Messy program with assertions -> proof -> verified program.
- practal 4y agoI am pretty sure that in 20 years every mathematician will happily use an ITP system. That is because formal reasoning is not unnecessary, but just too burdensome to be done on paper. Ideally a future ITP system will give you the formalisation almost for free, and lets you concentrate on your creative insights. It will be empowering you, instead of restricting you. It will be a tool that will let you explore your ideas more freely and creatively than it was possible before due to your limitations as a human. That is also why it is so important to get the basic foundations of such an ITP system right, as the limitations of the ITP system will become your limitations.