3 ms·

I find this very hopeful, as I feel that presentation should be a first-class consideration for these sorts of tools. Math is something that happens in the hum

I find this very hopeful, as I feel that presentation should be a first-class consideration for these sorts of tools. Math is something that happens in the human mind. It doesn't matter if the machine is uncovering the secrets of the Universe if no one can ever appreciate them, eh? I was explaining this to my sister this afternoon and to make the point I picked up a sliderule and slid the slipstick back and forth while pointedly not looking at the thing and asked her, "Am I doing math right now?" - - - - I'm trying to put together a simple, easy (relatively) to understand "stack" for this, starting with the theorem provers of Jens Otten: http://jens-otten.de/provers.html http://jens-otten.de/provers.html (See also "How to Build an Automated Theorem Prover" http://www.jens-otten.de/tutorial_tableaux19/ http://www.jens-otten.de/tutorial_tableaux19/ ) Prolog is a very simple language, the theorem provers are only a dozen lines of code or so, and the sequent calculus prover at least generates proofs that I personally find easy to follow. It doesn't go very far yet, but it's a start. Any information on formal methods and automated theorem proving would be much appreciated. (along the lines of: Concrete Semantics https://news.ycombinator.com/item?id=22074483 https://news.ycombinator.com/item?id=22074483 Metamath Zero, a bootstrapping theorem prover https://news.ycombinator.com/item?id=21358674 https://news.ycombinator.com/item?id=21358674 The Future of Mathematics? [video] https://news.ycombinator.com/item?id=21200721 https://news.ycombinator.com/item?id=21200721 "Building the Mathematical Library of the Future" https://news.ycombinator.com/item?id=25060613 https://news.ycombinator.com/item?id=25060613

cma 6y ago
> It doesn't matter if the machine is uncovering the secrets of the Universe if no one can ever appreciate them, eh? It's possible with access to something that almost serves as an oracle like this, we can use it prove deeper things that we do understand, with only the details of this one portion left un-understood. You could just assume a proposition is true or false, and do the same by working with the assumption, but that can quickly combinatorically explode with multiple propositions.
- carapace 6y ago
  Yes, but you still have a regress: you have to have good reason to trust the oracle. (E.g. Yin-Yang – A tool for stress-testing SMT solvers https://news.ycombinator.com/item?id=25123138 https://news.ycombinator.com/item?id=25123138 They found a bunch of bugs in Z3 and CVC4!)
lakecresva 6y ago
I wrote two reference type checkers for Lean and learned a lot about both the Lean kernel and the implementation of DTT; it's not an easy exercise, but I would recommend it. The ones I wrote are in a language that's not the easiest to read (though I did end up getting the performance to justify the language choice), but if any related questions come up feel free to contact me and I'll do my best to give a coherent answer: https://github.com/ammkrn/nanoda_lib https://github.com/ammkrn/nanoda_lib This paper on Lean's type theory dovetails nicely with any of the kernel implementations: https://github.com/digama0/lean-type-theory/releases/tag/v1.0 https://github.com/digama0/lean-type-theory/releases/tag/v1.... Also this article is really neat, thanks OP. These kinds of visual representations and other alternative mediums you can use to document stuff are (imo) a really important and under-explored area.
- carapace 6y ago
  Thanks!
nextos 6y ago
A similar book to Concrete Semantics, which I love, is Formal Reasoning about Programs by the same group the OP link comes from: http://adam.chlipala.net/frap/frap_book.pdf http://adam.chlipala.net/frap/frap_book.pdf ML for the Working Programmer is written by Paulson, one of the main persons behind Isabelle, and ends up with a prover project: https://www.cl.cam.ac.uk/~lp15/MLbook/ https://www.cl.cam.ac.uk/~lp15/MLbook/ Paulson teaches an undergrad course in Cambridge which is now using Huth & Ryan as a textbook. It's an incredible book that focuses on logic, SAT solvers and model checking. Probably the place to begin. An incomplete draft 2nd edition is in the authors website: ftp://ftp.cs.bham.ac.uk/pub/authors/M.D.Ryan/tmp/Anongporn/Ch1+3.pdf If you are interested in tableaux techniques, First-order Logic and Automated Theorem Proving by Fitting is a good text. Personally, I think the place to start from is Huth & Ryan. Logic is the calculus of CS. Then progress to type theory using a book like TAPL by Pierce or Proofs and Types by Girard. Then, depending on your interests, you can proceed to model checking, program analysis and theorem proving. For the first two, the classics are Katoen and Nielson & Nielson, respectively.
- carapace 6y ago
  Thank you!

cma 6y ago

> It doesn't matter if the machine is uncovering the secrets of the Universe if no one can ever appreciate them, eh? It's possible with access to something that almost serves as an oracle like this, we can use it prove deeper things that we do understand, with only the details of this one portion left un-understood. You could just assume a proposition is true or false, and do the same by working with the assumption, but that can quickly combinatorically explode with multiple propositions.

carapace 6y ago
Yes, but you still have a regress: you have to have good reason to trust the oracle. (E.g. Yin-Yang – A tool for stress-testing SMT solvers https://news.ycombinator.com/item?id=25123138 https://news.ycombinator.com/item?id=25123138 They found a bunch of bugs in Z3 and CVC4!)

lakecresva 6y ago

I wrote two reference type checkers for Lean and learned a lot about both the Lean kernel and the implementation of DTT; it's not an easy exercise, but I would recommend it. The ones I wrote are in a language that's not the easiest to read (though I did end up getting the performance to justify the language choice), but if any related questions come up feel free to contact me and I'll do my best to give a coherent answer: https://github.com/ammkrn/nanoda_lib https://github.com/ammkrn/nanoda_lib This paper on Lean's type theory dovetails nicely with any of the kernel implementations: https://github.com/digama0/lean-type-theory/releases/tag/v1.0 https://github.com/digama0/lean-type-theory/releases/tag/v1.... Also this article is really neat, thanks OP. These kinds of visual representations and other alternative mediums you can use to document stuff are (imo) a really important and under-explored area.

carapace 6y ago
Thanks!

nextos 6y ago

A similar book to Concrete Semantics, which I love, is Formal Reasoning about Programs by the same group the OP link comes from: http://adam.chlipala.net/frap/frap_book.pdf http://adam.chlipala.net/frap/frap_book.pdf ML for the Working Programmer is written by Paulson, one of the main persons behind Isabelle, and ends up with a prover project: https://www.cl.cam.ac.uk/~lp15/MLbook/ https://www.cl.cam.ac.uk/~lp15/MLbook/ Paulson teaches an undergrad course in Cambridge which is now using Huth & Ryan as a textbook. It's an incredible book that focuses on logic, SAT solvers and model checking. Probably the place to begin. An incomplete draft 2nd edition is in the authors website: ftp://ftp.cs.bham.ac.uk/pub/authors/M.D.Ryan/tmp/Anongporn/Ch1+3.pdf If you are interested in tableaux techniques, First-order Logic and Automated Theorem Proving by Fitting is a good text. Personally, I think the place to start from is Huth & Ryan. Logic is the calculus of CS. Then progress to type theory using a book like TAPL by Pierce or Proofs and Types by Girard. Then, depending on your interests, you can proceed to model checking, program analysis and theorem proving. For the first two, the classics are Katoen and Nielson & Nielson, respectively.

carapace 6y ago
Thank you!