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:

https://gitlab.com/hilbert-10/eucys-18

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.

—Chun

> Il giorno 01 mar 2019, alle ore 21:58, Makarius <makarius at sketis.net> 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: https://www.deepl.com
> 
> 
> 	Makarius
> 

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



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