全学自由研究ゼミナール　(証明の仕組み)

本セミナーは、数学におけるAI革命の最前線にあるLean証明支援ツールを使用した形式的な証明の作成に焦点を当て、1年生および2年生を対象としています。数学的な事前知識は一切必要なく、すべての学生が参加可能です。数学的厳密さを習得するだけでなく、論理的思考、問題解決能力、コーディングの精度を身につけることができ、これらはコンピュータサイエンス、データサイエンス、科学研究などの分野にも応用可能です。学生は、非形式的な推論を形式的な証明に変換し、Leanを活用して複雑な命題を検証する方法を学びます。これにより、数学的理解を深めるとともに、数学と新興技術の交差点で自分の立ち位置を確立できます。このコースは、形式的な手法とAIが数学の知識のアプローチや検証方法を再定義しつつある未来において、学生が活躍できる力を養います。