The Incredible Proof Machine (incredible.pm)

[David A. Wheeler]

FYI: I've just learned about The Incredible Proof Machine:

http://incredible.pm/

It's a very nice visual tool that might be useful for teaching the basics of how to create symbolic proofs. You basically drag blocks around and connect them.

--- David A. Wheeler

[Jon P]

That's pretty fun. I like the similarity with logic gates in circuits, it makes that connection very clear.

[vvs]

That's what I'm missing in Methamath. It's html representation is pretty good, but after using incredible.pm I'm addicted to visual graph representation. Especially its many little conveniences in UI, though it isn't perfect too.

[Antony Bartlett]

Yes, I'm also a big fan of The Incredible Proof Machine, which is why I wrote a program (graphmm) that can render Metamath proofs as graphs, e.g.

https://github.com/Antony74/graphmm/tree/master/output/essential/png

(The source code is at the root level of the same repository https://github.com/Antony74/graphmm )

Actually I just hacked an existing verifier (checkmm) to do this.

Getting this sort of visualization to be interactive though is more than I'm currently able contemplate taking on.

    Best regards,

        Antony

On Mon, Jun 17, 2019 at 3:08 PM vvs <vvs...@gmail.com> wrote:

That's what I'm missing in Methamath. It's html representation is pretty good, but after using incredible.pm I'm addicted to visual graph representation. Especially its many little conveniences in UI, though it isn't perfect too.

--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/5489d8fe-b6db-4a23-ba8b-fa12b8cd3feb%40googlegroups.com.

[vvs]

Getting this sort of visualization to be interactive though is more than I'm currently able contemplate taking on.

That looks really promising already. Let us hope someone will finish it someday.

[Tony]

How do I prove the last one in session 4: (A∨(A→⊥)→⊥)→⊥ ?

[vvs]

How do I prove the last one in session 4: (A∨(A→⊥)→⊥)→⊥ ?

Heh... That one looks daunting for some reason. But fear not, search for "Law of excluded middle implies double negation". Though, I was unable to find a solution until I solved it myself with much swearing and sweating :(

[vvs]

How do I prove the last one in session 4: (A∨(A→⊥)→⊥)→⊥ ?

Heh... That one looks daunting for some reason. But fear not, search for "Law of excluded middle implies double negation". Though, I was unable to find a solution until I solved it myself with much swearing and sweating :(

Correcting myself from creating even more confusion: it should be actually vice versa - "Double negation elimination implies law of excluded middle".

[Antony Bartlett]

That's the irrefutability of the law of the excluded middle, and yes it's probably the most difficult of the regular exercises.  Here you go

https://i.imgur.com/WIPJE8s.png

    Best regards,

        Antony

--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/65ae121f-beb9-4800-939e-93a20b0d3696%40googlegroups.com.

[vvs]

That's the irrefutability of the law of the excluded middle, and yes it's probably the most difficult of the regular exercises.  Here you go

BTW, if someone is still trying to solve it himself there is a hint in previous tasks. Look at De Morgan's law which convert disjunction into conjunction - it contains all the necessary steps. That's exactly how I was able to solve it.

[Tony]

I have solved it now. But not by myself. I used a proof on this page:  https://math.stackexchange.com/questions/140197/what-is-a-constructive-proof-of-lnot-lnotp-vee-lnot-p :

In Fitch style:

[vvs]

I have solved it now. But not by myself. I used a proof on this page:  https://math.stackexchange.com/questions/140197/what-is-a-constructive-proof-of-lnot-lnotp-vee-lnot-p :

The problem with different proofs is that they all are expressed in different languages. And to make a translation one must learn at least a subset of each one. Even professional mathematicians don't prove every single theorem by themselves - they learn most of them. So, you earned it by hard work and may be proud.

Congratulations.

[Tony]

It seems intuitively as a good idea at first to show proofs as images. But after using incredible.pm for a while I begin to think it only makes things harder. Proofs with more than six or seven blocks tend to turn in to a tangled mess. For the problems in session 5, I feel like wanting to solve them on paper first, using natural deduction.

[vvs]

It seems intuitively as a good idea at first to show proofs as images. But after using incredible.pm for a while I begin to think it only makes things harder. Proofs with more than six or seven blocks tend to turn in to a tangled mess. For the problems in session 5, I feel like wanting to solve them on paper first, using natural deduction.

I thought about that, but now I tend to disagree. Formulas are less effective in using space, i.e. they are linear and variables are often duplicated which makes theorems less clear and more ambiguous (they need an additional translation layer and taking precedence rules into account). Also, from experience I don't have problems with 20 or so steps per se when they are linear but they become difficult to understand when they are nested. But for nested steps it's better to use custom blocks (or lemmas) anyway. In any case graphs are more natural for inexperienced students because they lack syntax rules and are more intuitive. I find incredible.pm visual graph approach more natural than explicit stack machine. It's better to have more choice than not.