Proof Assistants at the interplay of mathematical cultures: a semiotic-cultural analysis of proof in higher education

大学数学の世界において、証明を行うという行為は単に問題を解くこと以上のものであり、一つの文化的実践である。それは、高校から高等教育へと進む学生たちが学ばなければならない、思考、記述、そしてアイデアを検証するための特定の作法である。何十年もの間、教育者たちは、学生たちが以前に学んだ直感的で非公式な議論と、大学レベルで求められる厳格で明示的な基準との間の溝を埋めるのに苦労する姿を見守ってきた。近年、この風景の中に新しいツールが登場した。それが「証明助手（プルーフ・アシスタント）」である。これらは数学的議論を絶対的な精度でチェックするために設計されたコンピュータプログラムであり、書き手に対して、一切のステップを説明なしに残さないことを強いるものである。これらのツールを数学をより厳密にするための手段と見る人もいれば、創造性を阻害したり、すでに苦戦している学生を混乱させたりすることを懸念する人もいる。問題は、単にこれらのプログラムが助けになるか妨げになるかではなく、証明が書かれ、理解されるという本質的な性質をどのように変えてしまうのかということである。

フランスの2つの大学の研究チームは、この相互作用を詳細に調査することに決めた。彼らは単に学生がより良く学んでいるかどうかを問うたのではなく、コンピュータプログラムが学生の思考プロセスをどのように作り変えるのかを観察した。研究は、学生が「Verbose Lean」と呼ばれる特定のタイプの証明助手を使用する、大学1年生の講義に焦榨された。標準的なプログラミング言語とは異なり、Verbose Leanは制御された自然言語の形式での記述を可能にするため、数学者が紙の上で話し、書く方法に近い感覚を与える。研究者たちは、一組の学生が古典的な問題に取り組む様子を観察した。それは、「数列が正の値に限りなく近づくならば、その数列の項は最終的に正自身にならなければならない」ということを証明するというものである。学生たちの会話、紙への書き殴り、画面へのタイピング、そしてコンピュータからのフィードバックを記録することで、研究者たちは、数学的なアイデアがいかにして粗削りな思考からコンピュータによって検証された事実へと旅をするのか、その詳細な地図を作成した。

研究者が発見したのは、コンピュータは単に最終的な答えをチェックするだけでなく、学生が通常は当たり前だとして見過ごしている隠れた仮定を明らかにする「鏡」として機能したということである。通常の数学の授業では、学生は小さな詳細をスキップしたり、あるステップが明白であるという「感覚」に頼ったりすることがある。しかし、コンピュータは、あらゆる対象、あらゆる条件、そしてあらゆる論理的な飛躍を、明示的に名付け、正当化することを要求する。研究は、この要求が一種の文化的転換を強いることを示した。学生たちは、自身の流動的で直感的なアイデアを、機械が理解できる厳格な構造へと翻訳しなければならなかった。このプロセスはスムーズなものではなかった。それは、学生たちの紙のメモ、語られる言葉、コンピュータのエラーメッセージ、そして教師の説明との間の、絶え間ない往復運動であった。

研究者たちは、学生たちの作業中に繰り返し現れた特定の数学的表現を追跡した。最初、学生たちはこの表現を、自身の推論に役立つ「数値」として扱っていた。しかし、それをコンピュータに入力しようとすると、プログラムはそれを拒絶した。コンピュータは、その数値が数学的に間違っていると言ったのではなく、その数値が「置かれるべき場所」が間違っていると言ったのである。学生たちは、その表現を数列における位置を示すラベルとして使おうとしていたが、コンピュータはその役割に対して整数を求めており、彼らの表現は分数であった。この瞬間が転換点となった。それは、証明助手の世界においては、数値がどのような役割を果たすかが、数値そのものと同じくらい重要であることを学生たちに気づかせたのである。彼らは戦略を練り直し、その表現を議論の別の部分へと移動させ、そこでようやくコンピュータの厳格なルールに適合させた。

この苦闘は、コンピュータ単独では解決されなかった。同じ教室の黒板の前で作業していた教師が、概念を視覚的に説明するために図を描いた。彼は、学生たちがなぜ自分たちの数値が目標値よりも小さくなければならないのかを理解するのに役立つ「窓」のサイズについて説明した。この視覚的な説明が、コンピュータによる最初の試みの拒絶と組み合わさることで、学生たちは思考を再編成することができた。彼らは最終的に、自分たちが格闘していた数値は、数列における「位置」ではなく、測定すべき「隙間の大きさ」であったことに気づいたのである。この切り替えを行ったとき、コンピュータは彼らの議論を受け入れた。最終的な証明は、アイデアから解決策への直線的な道のりではなく、記号の意味が、語られているのか、紙に書かれているのか、教師によって説明されているのか、あるいは機械によってチェックされているのかによって変化するという、複雑な旅路であった。

この研究は、証明助手が「エピステミック・レヴェレーター（認識的顕現者）」、つまり著者が用いる用語で、目に見えないものを可視化するツールとして機能することを示唆している。それらは、専門家や学生が当たり前すぎて語らない数学の「考えられなかった部分（unthoughts）」を明らかにする。伝統的な教室では、これらの空白は見過ごされるかもしれない。しかし、証明助手を備えた教室では、コンピュータがすべての空白を埋めるよう強制し、数学的正当性を支配する隠れたルールを露呈させる。研究者たちは、これはコンピュータが人間より優れているとか、人間がコンピュータより優れているということではないと主張している。むしろ、両方のシステムが協力して、異なる証明のあり方が衝突し、融合する新しい空間を作り出しているのである。

研究結果は、これらのツールの導入が高等教育における証明の文化を変えることを示している。それは単に技術的な厳密さを一段階加えることではなく、何が正しいとされるのかという理解の構成を組み替えることである。研究は、学生が単にコードの書き方を学ぶのではなく、異なる意味の世界の間を航行する方法を学んでいることを示している。彼らは、直感的な理解を機械が検証可能な言語へと翻訳すると同時に、教師による人間的な説明にも耳を傾けなければならない。コンピュータのエラーメッセージは単なる障害物ではなく、学生の理解がどこで不完全であるかを伝える信号なのである。暗黙の仮定を明示的なものにするよう強いることで、これらのツールは、数学的知識がいかに構築され、検証されるのかを研究するためのユニークな機会を提供している。

最終的に、論文は、証明助手が中立的なツールではないと結論づけている。それらは、何が妥当な議論としてカウントされるかについての特定の考えを携えている。学生がこれらを使用するとき、彼らは単に数学を学んでいるのではなく、どのように考え、どのようにコミュニケーションをとるかという、新しい文化的ルールを学んでいるのである。研究者たちは、この転換が、証明の教え方、専門家による実践のされ方、そして機械による検証のされ方の間の連続性と断絶を研究するための特権的な場を提供していると示唆している。この研究における学生たちの旅、すなわち初期の混乱から最終的な成功に至るまでの過程は、コンピュータと共に証明を学ぶことが「翻訳」のプロセスであることを物語っている。それは、数学的なアイデアの意味が、人間の直感、教師の指導、そして機械の精密さとの相互作用を通じて、テストされ、形を変え、最終的に安定していくプロセスなのである。