Email Gateway (Aug 22 2022 at 19:05): Email Gateway (Aug 22 2022 at 19:05):From: Makarius <makarius@sketis.net>
Dear German-speaking Isabelle users,
see this blog entry about the current issue of "Spektrum der
Wissenschaft 3.19":
https://sketis.net/2019/hilbert-and-isabelle-in-spektrum-der-wissenschaft-march-2019
(The blog entry is in English, the article in German.)
Makarius
Email Gateway (Aug 22 2022 at 19:15):From: "Chun Tian (binghe)" <binghe.lisp@gmail.com>
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
signature.asc
Email Gateway (Aug 22 2022 at 19:16):From: "Pal, Abhik" <ab.pal@jacobs-university.de>
I'm writing as one of the people involved in the formalization.
Since the Jugend Forscht project
<https://www.jugend-forscht.de/projektdatenbank/hilbert-meets-isabelle.html>
also received a nomination to the European Union Contest for Young
Scientists, we created a repository with a subset of the code. Most of
the actual code lives in a private repository and hasn't been made
public yet.
Hope that clears up the confusion.
Abhik
signature.asc
Email Gateway (Aug 22 2022 at 19:16):From: José Manuel Rodriguez Caballero <josephcmac@gmail.com>
Chun wrote:
“It’s good to know that formalizing mathematic theorems is still considered as scientific contributions.”
It is bad to know that non-formalizable mathematics is still accepted as a scientific contribution. Some important contemporary mathematician, whose name I will omit, told me:
“I do not think that the notion of invoking proof assistants and full formalizations to certify mathematics is a complete approach.
My stance is basically the same as Roger Penrose in his books on this question.
We do intend to formalize our mathematics, but it always has irreducible conceptual components that are just as important as the formalization.”
By the way, one of the entries in Archives of Formal Proofs was implemented using a book written by the mathematician that I quoted.
My opinion is that this is a myth. It is important to work in order to demystify mathematics, e.g., to invite mathematicians to use proof assistants in order to trust the software. It is possible to ban Roger Penrose books for a while? (Joke)
Kind Regards,
José M.
Sent from my iPhone
Email Gateway (Aug 22 2022 at 19:16):From: Makarius <makarius@sketis.net>
Also note that the full article needs to be paid for (and it is not
cheap). Only the initial blurp is free on the web.
Germans can go to a local bookstore and browse through the physical
magazine.
Makarius
Email Gateway (Aug 22 2022 at 19:17):From: Gert Smolka <smolka@ps.uni-saarland.de>
Dear All,
Larchey-Wendling and Forster recently finished a complete formalization of the Davis-Putnam-Robinson-Matiyasevich theorem (Hilbert’s 10th problem) in Coq. The paper is under review, the pdf is at http://www.ps.uni-saarland.de/Publications/documents/Larchey-WendlingForster_2019_H10_in_Coq.pdf. The theorems in the paper are linked to the Coq development so that the Coq code can be looked at online. The worked described in the paper contributes 12k loc to a Coq library of undecidable problems, see https://github.com/uds-psl/coq-library-undecidability.
Gert Smolka
Email Gateway (Aug 22 2022 at 19:17):From: Lawrence Paulson <lp15@cam.ac.uk>
“Irreducible conceptual components” sound too much like magic.
Larry Paulson
Email Gateway (Aug 22 2022 at 19:23):From: "Chun Tian (binghe)" <binghe.lisp@gmail.com>
It’s good to know that formalizing mathematic theorems is still considered as scientific contributions.
—Chun
(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)
signature.asc
Email Gateway (Aug 22 2022 at 19:24):From: Makarius <makarius@sketis.net>
You can try this automated tool: https://www.deepl.com
Makarius
signature.asc
Last updated: Nov 21 2024 at 12:39 UTC