Email Gateway (Aug 22 2022 at 16:44): Email Gateway (Aug 22 2022 at 16:44):From: Makarius <makarius@sketis.net>
Dear Isabelle users,
as the peak of the carnival season is approaching, it is a good time to
have latest deep learning technology produce some formal jokes for us
(before the .ai bubble bursts).
Presently the best translation service appears to be
https://www.deepl.com/translator so lets see if it can turn Isar proofs
into Coq (French) or Matita (Italian).
Here are some bits from
http://isabelle.in.tum.de/repos/isabelle/raw-file/Isabelle2017/src/HOL/Isar_Examples/Cantor.thy
theorem Cantor: "\<nexists>f :: 'a \<Rightarrow> 'a set. \<forall>A.
\<exists>x. A = f x"
proof
assume "\<exists>f :: 'a \<Rightarrow> 'a set. \<forall>A. \<exists>x.
A = f x"
then obtain f :: "'a \<Rightarrow> 'a set" where *: "\<forall>A.
\<exists>x. A = f x" ..
let ?D = "{x. x \<notin> f x}"
from * obtain a where "?D = f a" by blast
moreover have "a \<in> ?D \<longleftrightarrow> a \<notin> f a" by blast
ultimately show False by blast
qed
French:
théorème Cantor:"¡<<nexistes>f::' a \<Rightarrow>' a set. C'est tout ce
qui compte. Existe >x. A = f x"
preuve
supposer "{<existe>f::' a \<Rightarrow>' a set. C'est tout ce qui
compte. Existe >x. A = f x"
puis obtenez f:::"' a \<Rightarrow>' a set" où *:"\<<forall>A. Existe
x. A = f x"...
let? D = "{x. x \<notin> f x}"
à partir de * obtenir un où "? D = f a" par explosion
de plus ont "a \<in>? D \<<longleft à gauche flèche droite> a \<notin>
f a" by blast
finalement montrer False by blast
qed
Italian:
teorema Cantor:""<allegatoists>f::"a"<Rightarrow> "un set. "<forall>A.
"<esiste>x. A = f x x".
attestazione
assume ""<esiste>f::' a' a'"<Rightarrow>' un set. "<forall>A.
"<esiste>x. A = f x x".
quindi ottenere f::"a"<Rightarrow>' a set "dove *:""<forall>A.
"<esiste>x. A = f x"...
lasciare che D =" {x. x "<non> f x}".
da * ottenere un dove ". D = f = f a" per esplosione
inoltre hanno "un"<in>? D "<lunga freccia sinistra destra> un"<notin>
f a "da esplosione
infine mostrare Falso da esplosione
qed
I guess the problem to translate "let ?D = ..." properly into French is
due to the different spacing rules for ? (and !) in that language.
I also like the ultimate conclusion in Italian better: "infine mostrare
Falso da esplosione".
Makarius
Email Gateway (Aug 22 2022 at 16:44):From: Andrei Popescu <A.Popescu@mdx.ac.uk>
Funny how the Italian translation confuses blast with the explosion
principle (ex falso quodlibet).
Best regards,
Andrei
Email Gateway (Aug 22 2022 at 16:44):From: Makarius <makarius@sketis.net>
Feeding that back into the translation service leads this chain:
Isar: ultimately show False by blast
to Italian: infine mostrare Falso da esplosione
to German: Endlich mal falsch zeigen durch Explosion
to English: Finally sometimes false pointing by explosion
I must admit that the style of the machine translation has improved in
the past 10 years, but the old jokes from 20 years ago still work. Still
no "game changing" technology to be seen here ...
Makarius
Email Gateway (Aug 22 2022 at 16:44):From: Dominique Unruh <unruh@ut.ee>
Still no "game changing" technology to be seen here ...
Or is it a already sign of near human intelligence?
After beating us at chess and at go, now they beat us at Chinese whisper? :)
Best wishes,
Dominique.
Last updated: Nov 21 2024 at 12:39 UTC