The potential of automated reasoning tools to assist the working mathematician

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

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.