Re: [isabelle] “Hilbert and Isabelle” in Spektrum der Wissenschaft (March 2019)

I can also use Google Translate, thanks. Beside this, from your links I found their Git repository:

am I wrong that, so far they only wrote 2339 lines of proof scripts:

eucys-18/code$ wc -l *.thy
     109 CH2DigitComp.thy
     334 CH2Diophantine.thy
     142 CH2PositionalNotation.thy
     826 CH3ExponentialDiophantine.thy
     180 CH4ListableDiophantine.thy
      33 CH4PositionalEncoding.thy
     296 CH4RegisterMachine.thy
     419 CH4Simulation.thy
    2339 total

that doesn’t look like a deep proof of an important theorem, or they're still at early stage of the whole work.  Let me know I’m wrong please.


> Il giorno 01 mar 2019, alle ore 21:58, Makarius <makarius at> ha scritto:
> On 01/03/2019 21:56, Chun Tian (binghe) wrote:
>> (I purchased a copy of that PDF and saw that 6-pages article, although I don’t understand too much German - have to use dictionaries)
> You can try this automated tool:
> 	Makarius

Attachment: signature.asc
Description: Message signed with OpenPGP using GPGMail

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.