脳にとって「0の概念」は数の一種なのか? | Institute of Reproducing Kernels

Institute of Reproducing Kernels

色々な事を書きます。マイペースで書きます。

脳にとって「0の概念」は数の一種なのか?

 

英国のユニヴァーシティ・カレッジ・ロンドン(UCL)で行われた研究によって、ゼロを認識しているときの脳活動は「1」を思っているときの脳活動と最も近いことが判明しました。

また研究では、ゼロという概念に反応する脳活動が、動物にもともと備わっている「存在しないことを知覚する機能(知覚的不在)」に基づいている可能性が示されました。

一般的に、ゼロの概念はインドで「発明されたもの」と考えられていましたが、どうやらゼロを理解するための素質は、人間の脳に先天的にプレインストールされていたようです。

研究者たちは「現在の私たちが持つゼロの概念は、捕食者がいる状態「1」といない状態「0」を区別するための機能を、転用した可能性がある」と述べています。

https://nazology.net/archives/146657#%E8%84%B3%E3%81%AB%E3%81%A8%E3%81%A3%E3%81%A6%E3%80%8C0%E3%81%AE%E6%A6%82%E5%BF%B5%E3%80%8D%E3%81%AF%E6%95%B0%E3%81%AE%E4%B8%80%E7%A8%AE%E3%81%AA%E3%81%AE%E3%81%8B%EF%BC%9F

 

ゼロ除算の5W5H:

When: いつ 2014年2月2日

Where: どこで アヴェイロ大学 (ポルトガル)

Who: だれが  再生核研究所

What: 何を 0で割れないとされていたゼロ除算が、0で割れる考えがある事を発見した。

Why: なぜ  YAHOO知恵袋の質問に答えた際に考えた。

How: どのように  永い間研究してきた結果から、実は 当たり前であること に気が付いた。

HOW MUCH: 60兆円の価値です。

HOW MANY: 50億の人 (を1000年も引き付ける数学)小学生以上に影響を与える。ゼロで割れるようになった。

HOW LONG: 1000年以上 人類終末まで 不完全な四則演算 を完成させたから。ゼロ除算算法が 数学の基礎になる。

HOWinFUTURE: 数学と世界観の基礎になる。ゼロ除算算法が 数学の基礎になる。また、人間を自ら知らしめる素材になる。

2024.1.14.8:58 

 

Who defined Division by Zero as Infinity?

 

 

 

 

10年前のゼロ除算に関する最初の声明

https://ameblo.jp/syoshinoris/entry-12840277806.html

 

 

外国人「日本人って欧米人と接触する前から地球が丸いって知ってたの?」【海外反応】

https://masters.hiroshima-u.ac.jp/TSS-gakumon-sanpo/25-3-mizuta.pdf

そういう事じたい考えなかったと思います。

 

2021-04-20

1/0=0

Wikipediaにおける0除算解説

https://hoinori.hatenablog.com/entry/2021/04/20/075636

 

Terence Tao, "Machine Assisted Proof"

https://www.youtube.com/watch?v=AayZuuDDKP0

 

Coq QArith division by zero is zero, why?

Stack Overflow

https://stackoverflow.com › questions

このページを訳す

2015/03/26 — The short answer is: yes, it is absolutely safe. When we say that division by zero is not well-defined, what we actually mean is that zero ...

https://stackoverflow.com/questions/29282819/coq-qarith-division-by-zero-is-zero-why

 

 

 

彼らの分数 f(x,y) =x/y の定義と我々の拡張分数、割り算の定義は 同じである。 我々は高橋の一意性定理によって動機付けや山田体の構成で そう宣言した。ゼロ除算算法から基本性質を導いている。上記検証は我々の理論を保証している。 

沢山されているようである。2024.1.24.20:34

Isabelle20240124

Division by zero in type theory: a FAQ

Posted on July 5, 2020 by xenaproject

Hey! I heard that Lean thinks 1/0 = 0. Is that true?

Yes. So do Coq and Isabelle and many other theorem provers.

Doesn’t that lead to contradictions?

No. It just means that Lean’s / symbol doesn’t mean mathematical division. Let  denote the real numbers. Let’s define a function  by  if  and . Does making that definition give us a contradiction in mathematics? No, of course not! It’s just a definition. Lean uses the symbol / to mean . As does Coq, Isabelle etc. Lean calls it real.div by the way, not .

But doesn’t that lead to confusion?

It certainly seems to lead to confusion on Twitter. But it doesn’t lead to confusion when doing mathematics in a theorem prover. Mathematicians don’t divide by 0 and hence in practice they never notice the difference between real.div and mathematical division (for which 1/0 is undefined). Indeed, if a mathematician is asking what Lean thinks 1/0 is, one might ask the mathematician why they are even asking, because as we all know, dividing by 0 is not allowed in mathematics, and hence this cannot be relevant to their work. In fact knowing real.div is the same as knowing mathematical division; any theorem about one translates into a theorem about the other, so having real.div is equivalent to having mathematical division.

 

 

彼らの分数 f(x,y) =x/y の定義と我々の拡張分数、割り算の定義は 同じである。 我々は高橋の一意性定理によって動機付けや山田体の構成で そう宣言した。ゼロ除算算法から基本性質を導いている。上記検証は我々の理論を保証している。 

沢山されているようである。2024.1.24.20:34

 

 

なぜアインシュタインは天才と呼ばれたのか?

 

アインシュタインは、他の科学者達がとらわれていたある「常識」、普通はとらわれていることにすら気がつかないある「常識」、それに気づきそれを打ち破り「究極の発想の転換」をしたのです。 

このことが、アインシュタインが相対性理論を作り、二十世紀最高の天才と言われる理由なのです。2018/11/12

 

https://tenro-in.com/mediagp/readinglife-science/63425/#:~:text=%E3%82%A2%E3%82%A4%E3%83%B3%E3%82%B7%E3%83%A5%E3%82%BF%E3%82%A4%E3%83%B3%E3%81%AF%E3%80%81%E4%BB%96%E3%81%AE%E7%A7%91%E5%AD%A6,%E8%A8%80%E3%82%8F%E3%82%8C%E3%82%8B%E7%90%86%E7%94%B1%E3%81%AA%E3%81%AE%E3%81%A7%E3%81%99%E3%80%82

 

これはもっともなことだと思います。ゼロ除算も同じようではないでしょうか。

 

Division by zero is definable and possible

 

Einstein's Only Mistake: Division by Zero

http://refully.blogspot.com/2012/05/einsteins-only-mistake-division-by-zero.html

 

George Gamow (1904-1968) Russian-born American nuclear physicist and cosmologist remarked that "it is well known to students of high school algebra" that division by zero is not valid; and Einstein admitted it as {\bf the biggest blunder of his life} [1]1. Gamow, G., My World Line (Viking, New York). p 44, 1970.

 

ゼロ除算は実は簡単でした:0で割る事は、割らないことです:0はしないこと、できない事を表しています。

ゼロ除算は、 実は ゼロの意味 からも当たり前です:
ゼロで割ることは 割らないこと、したがって 割り当てられた数は無く、ゼロ。ゼロには、しないこと、できないことを表す 意味がある。
ゼロで割ることは 割らないこと、したがって 割り当てられた数は無く、ゼロ。ゼロには、しないこと、できないことを表す 意味がある。 ゼロ円あげるは、あげないことですね。ゼロ回施行は、しないことですね。 時速ゼロkmで走るは 止まっていて 走らないことを意味しますね。ですから、ゼロの意味を

https://ameblo.jp/syoshinoris/entry-12680138080.html

 

Isabelle (BSD-3, ML/Scala/Isabellemirror):

 (Univ. Cambridge, TU Munchen, Univ. Paris-Sud)

https://github.com/johnyf/tool_lists/blob/main/verification_synthesis.md#theorem-provers

 

培養脳細胞で「ChatGPTを超える」AI開発 豪スタートアップが13億円調達

https://news.yahoo.co.jp/articles/11a7436a6b2d396a2862cd51365c601eb7b0300b

 

0除算(0で割る行為)を認めてしまうと、 『数学の崩壊』・『世界の終わり』

https://twitter.com/Oita443256/status/1648222826946760704

 

それが常識でしたが、ゼロで割るには、自然な新しい意味があることが分りました。

現代数学の欠陥で 新世界を拓きます。 数学の夜明けです。 ご覧あれ

 

マスク氏、TruthGPTの開発表明「最大限に真実追求するAI」

https://news.yahoo.co.jp/articles/9b24e5931cd267d0ac5a430711e86c0739862f75

 

0除算はできましたか、

再生核研究所はできているが、正しいでしょうか。


 

 

 

Stephen Goree

 

B.S. in Mathematics, Western Washington University (Graduated 2019)Author has 79 answers and 22K answer views2y

Terence Tao points out in Analysis I that, starting from the Peano axioms and working from there up to a construction of the real numbers, you could possibly define a number system in which a/0 is defined for any number a…but then you’d end up with a system that doesn’t behave like the real numbers we’re familiar with. So essentially, that’s the answer to your question: you can’t in the real number system. You would have to define a completely new number system which doesn’t behave the same way the real numbers do.

866 views

View upvotes

https://www.quora.com/How-can-you-divide-by-zero?__nsrc__=4&fbclid=IwAR0NcvKGwaSRSlxOqyYfYEu1B97UMQnO0jnfEpHjgU9K32DFxDBL-u_TUzQ

 

If division by Zero were possible,then the result would exceed every integer

http://www.fen.bilkent.edu.tr/~franz/M300/zero.pdf   4/6

If division by Zero were possible,then the result would exceed every integer. An Early Reference to Division by Zero  C. B. Boyer4/6.

 

2023年11月24日 11時07分ソフトウェア

 

OpenAIが4度目のブレイクスルーとなる数学ができるAI「Q*(キュースター)」で汎用人工知能開発の飛躍を目指す、

アルトマンCEO解任騒動の一因か

https://gigazine.net/news/20231124-open-ai-q-star/#google_vignette

 

イサベルホルは、相当進んでいるのではないでしょうか。

 

 

初めて飛行機を作って乗った方、車を初めて作って乗った方を見たとき、人はどうして今日のような時代を迎えるだろうと想像できたでしょうか。ゼロ除算の世界は 真に新しい世界、その世界を覗かないで どうしてゼロ除算の世界について想像したり、語れるでしょうかhttps://ameblo.jp/syoshinoris/entry-12490439836.html

 

ゼロ除算は、 実は ゼロの意味 からも当たり前です:
ゼロで割ることは 割らないこと、したがって 割り当てられた数は無く、ゼロ。ゼロには、しないこと、できないことを表す 意味がある。
ゼロで割ることは 割らないこと、したがって 割り当てられた数は無く、ゼロ。ゼロには、しないこと、できないことを表す 意味がある。 ゼロ円あげるは、あげないことですね。ゼロ回施行は、しないことですね。 時速ゼロkmで走るは 止まっていて 走らないことを意味しますね。ですから、ゼロの意味を

https://ameblo.jp/syoshinoris/entry-12680138080.html

 

 

引用されている論文が出ました。

 

 

中国の研究チームが達成した「量子超越性」が意味すること

スパコンで20億年以上の計算を3分強で

https://news.yahoo.co.jp/.../aca92e377336a2c16ca10fa2adbb...

凄いですね:0除算はできるでしょうか:

 

 

 

どうでしょうか???

1999年には、アメリカ合衆国の雑誌である『ライフ』の企画「この1000年で最も重要な功績を残した世界の人物100人」で、日本人として唯一86位にランクインした。 葛飾北斎

https://ja.wikipedia.org/.../%E8%91%9B%E9%A3%BE%E5%8C%97...

 

The Institute of Reproducing Kernels is dealing with the theory of division by zero calculus and declares that the division by zero was discovered as 0/0=1/0=z/0=0 in a natural sense on 2014.2.2. The result shows a new basic idea on the universe and space since Aristotelēs (BC384 - BC322) and Euclid (BC 3 Century - ), and the division by zero is since Brahmagupta (598 - 668 ?).

 

再生核研究所声明 477(2019.2.23) ケンブリッジ大学とミュンヘン工科大学のIsabelle 計算機システムはゼロ除算x/0=0 を導いた

再生核研究所声明 479(2019.3.12)  遅れをとったゼロ除算 - 活かされない敗戦経験とイギリスの畏れるべき戦略/0=0 を導いた

 

Black holes are where God divided by 0

ゼロ除算(division by zero)1/0=0/0=z/0=\tan(\pi/2)=0、log0=0

 

 

【量子力学】Google、ついに世界初の「量子超越性」実証か 約1万年かかる計算を、3分20秒で終える[9/22]

http://itest.5ch.net/.../read.../scienceplus/1571396462/-100 …

「ゼロ除算が割り切れる時代が来たか」 「え?」

https://twitter.com/.../status/1185245335532134400/photo/1

 

 

万能AIがもたらす未来 物理法則を発見する可能性も

3Graphics

https://www.nikkei.com/article/DGXZQOCD0756V0X01C23A2000000/

 

ゼロ除算は、30年も前に予告していたイサベルホル、人間が理解できなかった。

 

 

生成系AIに興味のある全ての方へ

アマゾンウェブサービスジャパン

https://aws.amazon.com/jp/events/aws-innovate/apj/aiml-data/?trkCampaign=innovate-aiml-apj&trk=fc3630de-ccf3-48a9-8e1c-283528af31d4&sc_channel=display+ads&sc_publisher=yda

 

ニュートンとアインシュタインの重力理論が崩壊している連星を発見!

https://nazology.net/archives/143351#google_vignette

 

ゼロ除算の応用できないですか。ゼロ除算で解決できないですか。

 

 

 

ゼロ除算とは何か

それはゼロで割ることである。ゼロで割る事とは何か。 

その定義、意味が 問題である。

それを普通の掛け算の逆と考えれば、それはできないとか、定まらないと なり、それが永い間の世の常識である。

ところがゼロで割るという意味には、割ることの意味を 自然に拡張(ある一般的な意味における割る意味で)、あるいは そもそもゼロの意味から、考えると、ゼロ除算は何時でも可能で、何時でも ゼロで割ればゼロである という美しい数学が 2014.2.2.に発見された。 それを発展させた ゼロ除算算法 は 数学の基礎に甚大な影響を与え、数学ばかりではなく、人生観、世界観に 甚大な影響を与えることは分かってきた。

特に、数学は そもそも基本的な欠陥を有している と言える。

2024.1.10.5:46

 

何故ゼロ除算が不可能であったか理由

 

1 割り算を掛け算の逆と考えた事

2 極限で考えようとした事

3 教科書やあらゆる文献が、不可能であると書いてあるので、みんなそう思った。

 

Matrices and Division by Zero z/0 = 0

http://file.scirp.org/pdf/ALAMT_2016061413593686.pdf

 

「マイクロソフト」「Google」「AmazonAI三つ巴戦の行方は? 超絶進化で仕事は奪われサイバー犯罪も激増?https://news.yahoo.co.jp/articles/78d81b626b1ead633347f036e78d32db918f91eb

 

キラー問題もスラスラ「韓国製数学AI」、ChatGPT抜き世界評価1位

https://news.yahoo.co.jp/articles/7bf80224fc9de6702d7540c6a78d3bd693619106

 

 

 

 

インド出身の偉大な 世界的な 指導的な数学者が、ゼロ除算の我々の発見の凄さ を認識したようである。

2024.1.15.8:42

 

I am surprised to have your mail again. I am happy and fully convinced with the great work of scholars Brahmagupta, Bhaskara II, Mahavira, Aristotle, Cauchy, Weierstrass, Euler, Newton, Bernoulli, and their numerous followers. They laid the correct foundation of Mathematics by showing that 0/0 is indeterminant, i.e., it is defined only in the limiting sense.

 

You will be able to contribute to mathematics on world history with India's great and long hirosophy.

We Japanese studied deeply from India.

 

I expect your contribution to the division by zero.

My feelings are almost void.

 

NOT LIMITTING!!!!

I attached one typical evidence.

2024.1.15.8:30

 

 

東大合格率とゼロ除算:

 

ある名門高校の東大合格率は40%だという。 これは架空の話しであるが 東大受験した高校生の合格率と考えれば ありそうな話しであろう。 合格しなそうな人は 受験しないからである。名門校となれば データや経験から、合格率を高められるだろう。

 問題は、受験生がゼロの時、合格率はどのようになるだろうか。

現代数学では、考えてはならないとなっている。ゼロで割れないからである。

 

歴史上はじめて 宣言された我々のゼロ除算では、合格率は ゼロとなる。

世相でも 良い結果ではないだろうか。ゼロ除算不可能を 可能にしている。

ついでに 私の理解に寄れば、 母校の中学は 再編後前も 歴史上 東大受験生は唯一人で 合格している。

東大合格率は100%である。 甥の同級生で子供のころから 神童の誉が高かった。

母校の高校 再編後前も 歴史上 東大受験生は ゼロで、従って東大合格率は ゼロである。 

買い物から帰って この構想が湧いた。

2024.1.18.12:34

 

初めて飛行機を作って乗った方、車を初めて作って乗った方を見たとき、人はどうして今日のような時代を迎えるだろうと想像できたでしょうか。ゼロ除算の世界は 真に新しい世界、その世界を覗かないで どうしてゼロ除算の世界について想像したり、語れるでしょうかhttps://ameblo.jp/syoshinoris/entry-12490439836.html

 

 

ゼロ除算は、 実は ゼロの意味 からも当たり前です:
ゼロで割ることは 割らないこと、したがって 割り当てられた数は無く、ゼロ。ゼロには、しないこと、できないことを表す 意味がある。
ゼロで割ることは 割らないこと、したがって 割り当てられた数は無く、ゼロ。ゼロには、しないこと、できないことを表す 意味がある。 ゼロ円あげるは、あげないことですね。ゼロ回施行は、しないことですね。 

時速ゼロkmで走るは 止まっていて 走らないことを意味しますね。ですから、ゼロの意味を

https://ameblo.jp/syoshinoris/entry-12680138080.html

 

 

 

「生成AIは100%数学でできている」現役スタンフォード生が語るAI時代の算数力

https://dime.jp/genre/1720142/#google_vignette

 

感じは分かりますが、そこまで言えるでしょうか。

 

 

In proof assistants[edit]

Many proof assistants, such as Coq and Lean, define 1/0 = 0. This is due to the requirement that all functions are total. Such a definition does not create contradictions, as further manipulations (such as cancelling out) still require that the divisor is non-zero.[33][34]

  1.  Tanter, Éric; Tabareau, Nicolas (2015), "Gradual certified programming in coq", DLS 2015: Proceedings of the 11th Symposium on Dynamic Languages, Association for Computing Machinery, arXiv:1506.04205doi:10.1145/2816707.2816710, The standard division function on natural numbers in Coq, div, is total and pure, but incorrect: when the divisor is 0, the result is 0.
  2. ^ Buzzard, Kevin, "Division by zero in type theory: a FAQ", Xena Project (Blog), retrieved 2024-01-21

https://en.wikipedia.org/wiki/Division_by_zero

 

 

 

ゼロ除算(ゼロじょさん、0除算、英語: division by zero)とは、0で除す割り算のことである。

このような除算は除される数をaとするならば、形式上は a/0と書くことが ...

関連する質問

0は除算できないのはなぜ?

0による除算とは何ですか?

 

ゼロ除算は可能か?

ゼロ除算は可能で、正解はゼロです。 何を0で割っても ゼロです。

ゼロ除算は可能で、正解はゼロです。 何を0で割っても ゼロです。2022/04/22

ゼロ除算は可能で、正解はゼロです。 何を0で割っても ゼロです。

ゼロ除算の対応は?

 

ゼロに対応する点は無限遠点で、1/0=∞ と考えられてきた。 オイラー、アーベル、リーマンの流れである。 ところが、ゼロ除算は1/0=0 で、実は無限遠点はゼロに対応していることが確認された。2022/04/22

 

ゼロ除算は可能で、正解はゼロです。 何を0で割っても ゼロです。

ゼロ除算は可能か?

ゼロ除算は可能で、正解はゼロです。 何を0で割っても ゼロです。

ゼロ除算は可能で、正解はゼロです。 何を0で割っても ゼロです。2022/04/22

linkedin.com

https://jp.linkedin.com › pulse › ゼロ除算は可能で正解...

 

検索ゼロ除算は可能か?

 

 

0の新しい意味の発見、0の意味から当たり前

 

0は できないこと、しないこと、を現す意味をもつ。

0で割る事は割らないことで、したがって

割り当てられた数はない。

すなわち、0除算は0です。

何を0で割っても0です。

 

100割る0は?

この意味で割り算の意味を考えれば、100割る0は 0 であるとなる。2022/04/19

記号∞ (アーベルなどはこれを 1 / 0 のように表記していた)で表す。

https://www.google.co.jp/search?sca_esv=593347961&hl=ja&q=%E3%82%BC%E3%83%AD%E3%82%92%E5%89%B2%E3%82%8B&sa=X&ved=2ahUKEwi1pb26j6eDAxWdhq8BHQSEAMUQ1QJ6BAg2EAE&biw=1600&bih=773&dpr=1

a がゼロでなければ、分数b/aは 現代数学の定義と同じに定義される。 100割るゼロはゼロ、すなわち、100/0=0である。2021/11/28

1970年代の教科書でも、ゼロ除算の扱いは同様である ...

 

 

 

天文】宇宙にあるブラックホールの数は推定4,000京個 

https://tabi-labo.com/302577/wt-black-hole-number

 

 

The Institute of Reproducing Kernels is dealing with the theory of division by zero calculus and declares that the division by zero was discovered as $0/0=1/0=z/0=0$ in a natural sense on 2014.2.2. The result shows a new basic idea on the universe and space since Aristotele (BC384 - BC322) and Euclid (BC 3 Century - ), and the division by zero is since Brahmagupta (598 - 668 ?).

 

Announcement 478: Who did derive first the division by zero 1/0 and the division by zero calculus $\tan(\pi/2)=0, \log 0=0$ as the outputs of a computer?

 

天文】宇宙にあるブラックホールの数は推定4,000京個 

https://tabi-labo.com/302577/wt-black-hole-number

 

\author{{\it Institute of Reproducing Kernels}

Kawauchi-cho, 5-1648-16,

Kiryu 376-0041, Japan\\

}

\date{2021.1.26.}

\maketitle

 

 

The Institute of Reproducing Kernels is dealing with the theory of division by zero calculus and declares that the division by zero was discovered as $0/0=1/0=z/0=0$ in a natural sense on 2014.2.2. The result shows a new basic idea on the universe and space since Aristotele (BC384 - BC322) and Euclid (BC 3 Century - ), and the division by zero is since Brahmagupta (598 - 668 ?).

 

Announcement 478: Who did derive first the division by zero 1/0 and the division by zero calculus $\tan(\pi/2)=0, \log 0=0$ as the outputs of a computer?

 

 

世界を変えた等式17: 素晴らしい。

 

しかしながら、アリストテレス(紀元前384年-紀元前322年)以来 否定され、天才オイラーの間違いを含み、アインシュタインの生涯の懸案だったとされるゼロ除算が 含まれていない。惜しいかな数学。四則演算が不完全だった。

そこで 下記の公式は、17に続く等式と すべきではないでしょうか。

 

 

1/0=0/0=0,

tan (\pi/2)=0,

log 0=0,

(f(x)/x)(0) = f^\prime(0) = f’(0)

 

2022.2.8.06:00

 

 

The equation that changed the world 17: Great.

 

However, it has been denied since Aristotle (384 BC-322 BC), including the mistake of genius Euler, and does not include division by zero, which is said to have been a concern for Einstein's life. A regrettable math. The four arithmetic operations were incomplete. Therefore, the following formula should be the equation following 17.

 

1/0 = 0/0 = 0,

tan (\ pi / 2) = 0,

log 0 = 0,

(f (x) / x) (0) = f ^ \ prime (0) = f ’(0)

 

2022.2.8.06:00

 

ゼロ除算の5W1H

 

When:いつ 2014年2月2日

Where:どこで アヴェイロ大学 (ポルトガル)

Who: だれが  再生核研究所

What: 何を 0で割れないとされていたゼロ除算が、0で割れる考えがある事を発見した。

Why: なぜ  YAHOO知恵袋の質問に答えた際に考えた。

How: どのように  永い間研究してきた結果から、実は 当たり前であること に気が付いた。

 

 

 

Leanは プログラミング言語および証明支援系(theorem prover)英語版)である。

帰納型英語版)を伴うCalculus of constructions英語版)に基づく。

解説[編集]

LeanプロジェクトはGitHubでホストされているオープンソース英語版)・プロジェクトである。2013年にMicrosoft ResearchのLeonardo de Mouraによって立ち上げられた[1]

https://ja.wikipedia.org/wiki/Lean_(%E8%A8%BC%E6%98%8E%E3%82%A2%E3%82%B7%E3%82%B9%E3%82%BF%E3%83%B3%E3%83%88)

 

 

 

 

The Coq Proof Assistant: Welcome!

Coqは、証明支援システムの一つ。Coqの核はプログラミング言語Gallina英語版)を用いる。フランス国立情報学自動制御研究所PI.R2チーム(PPS研究所内にある)が、エコール・ポリテクニークフランス国立工芸院パリ第7大学パリ第11大学と(かつてリヨン高等師範学校とも)共同して開発している。Hugo Herbelinが事実上の開発代表者である。

https://ja.wikipedia.org/wiki/Coq

 

 

 

 

The Isabelle[a] automated theorem prover is a higher-order logic (HOL) theorem prover, written in Standard ML and Scala. As an LCF-style theorem prover, it is based on a small logical core (kernel) to increase the trustworthiness of proofs without requiring — yet supporting — explicit proof objects.Isabelle is available inside a flexible system framework allowing for logically safe extensions, which comprise both theories as well as implementations for code-generation, documentation, and specific support for a variety of formal methods. It can be seen as an IDE for formal methods. In recent years, a substantial number of theories and system extensions have been collected in the Isabelle Archive of Formal Proofs (Isabelle AFP)[2]

https://en.wikipedia.org/wiki/Isabelle_(proof_assistant)