GeoCoq
What books were used to make GeoCoq?
I see here mention of Metamathematische Methoden in der Geometrie (German). Did you use that version or did you use a version in English which could be purchased online? I would like to follow along and see how the proofs/definitions/etc. were translated from natural language into Coq if possible :)
Looking forward to your response!
Dear Lance,
Unfortunately up to my knowledge there is currently no English translation of Metamathematische Methoden in der Geometrie .
But according to Michael Beeson:
"Marvelously and miraculously, a former graduate student of Tarski (Kenneth Driessel, who was in Tarski's seminar 1962-64 but finished at U. of Oregon) has stepped forward and volunteered to finance an English translation of SST, in the sense of paying for translation and putting the result into LaTeX. »
I just asked Michael if he had news about this project.
Cheers,
Julien
Le 3 juin 2021 à 02:05, Lance Pollard @.***> a écrit :
I see here http://geocoq.github.io/GeoCoq/ mention of Metamathematische Methoden in der Geometrie (German). Did you use that version or did you use a version in English which could be purchased online? I would like to follow along and see how the proofs/definitions/etc. were translated from natural language into Coq if possible :)
Looking forward to your response!
— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/GeoCoq/GeoCoq/issues/35, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAIYG7PSASGD4Q2EWXISRGLTQ3BK3ANCNFSM457WNIUQ.
Dear Lance, dear Julien,
I had asked Michael in early February and then Part I of the book was already translated. Michael said to the people translating it that it could be published on its own. Let's see what is new once Julien ears back from him.
Cheers, Pierre
Dear @lancejpollard,
Can I close this issue?
I could ask Michael if some translation got published.
Cheers, Pierre
