The potential of automated reasoning tools to assist the working mathematician

大多数最近被证明的重要数学定理都有几百页的证明，并且不能被裁判可靠地验证。在这种情况下，开发一个用户友好的，正式的，证明助手，每个人都可以检查他的结果证明，成为数学的未来至关重要。有Isabelle、HOL、Coq等多个证明助手，但它们目前对工作的数学家没有吸引力。因此，形式化的数学结果库并不丰富，不足以形式化大多数严肃的数学结果，更重要的是，这些证明助手的开发人员没有从数学家那里得到足够的反馈。在本项目中，我们的目标是在Isabelle中形式化凸分析和优化理论，这是VR的专业领域之一。这将显着改善伊莎贝尔的图书馆，因为凸优化技术是目前的核心技术之一，解决优化问题的数学和应用，并将形成基础，进一步重要的数学形式化。更重要的是，我们的目标是向Isabelle和Proof General开发人员提供详细的反馈，描述系统中应该改进的地方，使其对数学家更具吸引力。在此基础上，我们将修改Isabelle的文档及其Proof General界面，以生成针对工作数学家的版本。

Most of the recently proved important mathematical theorems have proofs of several hundreds of pages and cannot be reliably verified by referees. In this context, developing a user-friendly, formal, proof assistant, where everyone can check a proof of his result, becomes vital for the future of mathematics. There exist several proof assistants, such as Isabelle, HOL, Coq, etc., but they are currently unattractive for working mathematicians. As a result, libraries of formalized mathematical results are not sufficiently rich to formalize most serious mathematical results, and, more importantly, developers of these proof assistants do not have sufficient feedback from mathematicians.In this project, we aim to formalize the theory of convex analysis and optimization in Isabelle, which is one of the areas of expertise of the VR. This will significantly improve Isabelle's library, since convex optimization techniques are currently one of the central techniques for addressing optimization problems in mathematics and applications, and will form the basis for further important mathematical formalisations. More importantly, we aim to provide detailed feedback to Isabelle and Proof General developers, describing what should be improved in the system to make it more attractive to mathematicians. Building on this critique, we will revise the documentation of Isabelle, and its Proof General interface, to produce versions targeted at working mathematicians.