Toward a formal proofs and automated verifications of discrete mathematics

2014 Fiscal Year Final Research Report

• Project/Area Number: 25610034
• Research Category: Grant-in-Aid for Challenging Exploratory Research
• Allocation Type: Multi-year Fund
• Research Field: Foundations of mathematics/Applied mathematics
• Research Institution: Kyushu University
• Principal Investigator: MIZOGUCHI Yoshihiro 九州大学, マス・フォア・インダストリ研究所, 准教授 (80209783)
• Project Period (FY): 2013-04-01 – 2015-03-31
• Keywords: 数理論理学 / 数学の形式化 / 検証可能証明 / ソフトウェア検証 / 離散数学 / 計算理論

Outline of Final Research Achievements

Our main results include a formalization of finite automata, sticker system and Fuzzy database as a formal specification of mathematics of discrete objects. A successful international workshop about "Theorem proving and provers for reliable theory and implementations" were held with over 80 participants including engineers in companies and researchers of computer science and mathematics. The famous unsolved problem for more than 400 years ago, Kepler conjecture was solved by Thomas Hales using formalized proofs last year. We publicized their result with introductions. Further, we appealed the importance and future view of the formalization of mathematics especially to students and teachers who are going to study mathematics in future.

Free Research Field

理論計算機科学