「理系が恋に落ちたので証明してみた」というアニメを見てみました。
I saw an animation whose title is "A couple of science human, fell in love, so they try to prove the existence of love."
このアニメの脚本を私が書くとしたら(まあ、ありえませんが)、
If I were to write a script for this anime (Of couse it will not), the title may be
「理系が恋に落ちたので計算(シミュレーション)してみた」
"A couple of science human, fell in love, so they try to calculate the existence of love."
になるだろうなぁ、と思っています。
これが、数学者とエンジニア(工学者)の違いです。
This is the difference between mathematicians and engineers.
数学者の「証明」とは、時間的、空間的に絶対普遍の、(主に数学を使った)真理の追求のメソッドですが、
Mathematician proof is a method of pursuing truth (mainly using mathematics) that is absolutely universal in time and space, however,
工学者の「計算」とは、限定的な時空間内で、有用であるかどうかを確認するメソッドです。
Engineer's "calculation" is a method that checks whether it is useful in a limited space-time.
どちらが優れているということはなく、そもそも目的が違うのです。
Neither is superior, and the purpose is different primarily.
-----
無粋ですが、エンジニアの一人として、第1話の冒頭の主人公たちのセリフに突っ込んでみたいと思います。
This is a tactless question, however, as an engineer, I'd like to dig into the messages of the main characters at the beginning of Episode 1.
■「多項式時間帰着」
"Polynomial time return"
この話の中では、「今日の帰宅時までに、パソコンを使って、計算が終わるアルゴリズムのプログラム」という理解で、良いです。
In this story, it is good to understand that "an algorithm program using a personal computer, that can complete the calculation by returning home"
この逆は「1億年後に計算が終わらないアルゴリズムのプログラミング」です。
The opposite is "an algorithm programming that does not finish in 100 million years."
■「ハミルトンパス」
"Hamilton Pass"
複数の都市の全部を1回だけ通過する経路(パス)のこと、または、そのようなパスを算出するアルゴリズムのこと、です。
A path that passes through all of a plurality of cities only once, or an algorithm that calculates such a path.
「NP問題」とか「NP証明」とかでググると、上記の言葉が出てきます。
Googling for "NP problem" or "NP proof", the above words come out.
-----
ところで、原則として、数学の証明は、コンピュータで求めることはできません。
By the way, as a general rule, proof of mathematics cannot be obtained by computer.
コンピュータの計算は、有限時間の中での、有限回数のパターンを試せるだけです。
Computer calculations can only try a finite number of patterns in a finite amount of time.
それは、解空間のほんの一部をチェックしたものに過ぎないからです。
Because it's just looking for a small part of the solution space.
ですが、アニメを見る限り、彼ら彼女らは、パソコンを使って「何か」を求めているようです。
However, as far as anime is concerned, they seem to be asking for "something" using a personal computer.
「何をしているんだろう」と思っています。
I think "what they are doing".
(Continuation from yesterday)