*To*: isabelle-users <isabelle-users at cl.cam.ac.uk>*Subject*: [isabelle] The Incredible Proof Machine*From*: Joachim Breitner <breitner at kit.edu>*Date*: Thu, 24 Sep 2015 16:54:08 +0200

Hi, this is slightly off topic and in no way related to the recent discussion about foundations and certification, but I created a new theorem prover. But first things first: (The following text is also on my blog at https://www.joachim-breitner.de/blog/682) In a few weeks, I will have the opportunity to offer a weekend workshop to selected and motivated high school students to a topic of my choice. My idea is to tell them something about logic, proofs, and the joy of searching and finding proofs, and thegratification of irrevocable truths. While proving things on paper is already quite nice, it is much more fun to use an interactive theorem prover, such as Isabelle, Coq or Agda: You get immediate feedback, you can experiment and play around if you are stuck, and you get lots of small successes. Someone once called interactive theorem proving âthe worlds most geekiest videogameâ. Unfortunately, I donât think one can get high school students without any prior knowledge in logic, or programming, or fancy mathematical symbols, to do something meaningful with a system like Isabelle, so I need something that is (much) easier to use. I always had this idea in the back of my head that proving is not so much about writing text (as in ânormally writtenâ proofs) or programs (as in Agda) or labeled statements (as in Hilbert-style proofs), but rather something involving facts that I have proven so far floating around freely, and way to combine these facts to new facts, without the need to name them, or put them in a particular order or sequence. In a way, Iâm looking for labVIEW wrestled through the Curry-Horward-isomorphism. So I set out, rounded up a few contributors, implemented this idea, and now I proudly present: The Incredible Proof Machine http://incredible.nomeata.de/ This interactive theorem prover allows you to do perform proofs purely by dragging blocks (representing proof steps) onto the paper and connecting them properly. There is no need to learn syntax, and hence no frustration about getting that wrong. Furthermore, it comes with a number of example tasks to experiment with, so you can simply see it as a challenging computer came and work through them one by one, learning something about the logical connectives and how they work as you go. For the actual workshop, my plan is to let the students first try to solve the tasks of one session on their own, let them draw their own conclusions and come up with an idea of what they just did, and then deliver an explanation of the logical meaning of what they did. The implementation is heavily influenced by Isabelle: The software does not know anything about, say, conjunction (â) and implication (â). To the core, everything is but an untyped lambda expression, and when two blocks are connected, it does unification of the proposition present on either side. This general framework is then instantiated by specifying the basic rules (or axioms) in a descriptive manner. It is quite feasible to implement other logics or formal systems on top of this as well. At this point I must thank Tobias for writing up his pattern unification algorith so nicely back then: http://www21.in.tum.de/~nipkow/pubs/lics93.html Another influence of Isabelle is the non-linear editing: You neither have to create the proof in a particular order nor have to manually manage a âproof focusâ. Instead, you can edit any bit of the proof at any time, and the system checks all of it continuously. As always, I am keen on feedback. Also, if you want to use this for your own teaching or experimenting needs, let me know. We have a mailing list for the project, the code is on GitHub, where you can also file bug reports and feature requests. Contributions are welcome! All aspects of the logic are implemented in Haskell and compiled to JavaScript using GHCJS, the UI is plain hand-written and messy JavaScript code, using JointJS to handle the graph interaction. Obviously, there is still plenty that can be done to improve the machine. In particular, the ability to create your own proof blocks, such as proof by contradiction, prove them to be valid and then use them in further proofs, is currently being worked on. And while the page will store your current progress, including all proofs you create, in your browser, it needs better ways to save, load and share tasks, blocks and proofs. Also, weâd like to add some gamification, i.e. achievements (âFirst proof by contradictionâ, â50 theorems provenâ), statistics, maybe a âshare theorem on twitterâ button. Enjoy! Joachim -- Dipl.-Math. Dipl.-Inform. Joachim Breitner Wissenschaftlicher Mitarbeiter http://pp.ipd.kit.edu/~breitner

**Attachment:
signature.asc**

**Follow-Ups**:**Re: [isabelle] The Incredible Proof Machine***From:*Peter Lammich

**Re: [isabelle] The Incredible Proof Machine***From:*Christian Sternagel

**Re: [isabelle] The Incredible Proof Machine***From:*Andrei Popescu

- Previous by Date: Re: [isabelle] find_consts does not find constants from BNF package
- Next by Date: Re: [isabelle] The Incredible Proof Machine
- Previous by Thread: Re: [isabelle] Fwd: Sledgehammer all subgoals?
- Next by Thread: Re: [isabelle] The Incredible Proof Machine
- Cl-isabelle-users September 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list