[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] [Dr. TLA+ Series] Paxos - Andrew Helwer (June 22nd, 10-11:30am PDT)

   How to Write a 21st Century Proof
      (The video is in a format my browser can't read.)

I have written a proof using this method.


The references are to metamath. (Not sure they are still up to date.)


In my opinion, you need a specific editor to write this kind of proof. Writing it
as a latex text in a normal editor is very demanding even with the system of abbreviation
proposed by pf2.

When I was in high school, my main problem (one of my main problems to be honest) was
to deal with  all those hypotheses that pop in an out during the proof. Sometimes you could
use them, sometimes you couldn't. With  the model of proof proposed here and its hierarchy,
I would have understood.
   A Mathematical View of Computation

This is this one that I had seen. Very beautiful talk. A link to it deserves to be kept somewhere in an official
html page so that we can access it easily.

In fact they nearly have the kind of index I was asking for since it is possible to choose the slide and the
part of the talk referring to it begins.