SHF: Small: MaPaMaP: Massively Parallel Solving of Math Problems

最先进的自动化定理证明工具已经取得了进展，并在某些情况下解决了长期未解决的数学问题，如：能否将正整数分为两个桶，这样两个桶都不包含毕达哥拉斯三重（a ^2+b^2=c^2的解），或者平面上的点可以涂上5种颜色，这样距离为1的每两个点都有不同的颜色？同样的技术在工业中验证硬件和软件也是至关重要的。机械化数学最近和未来成功的一个关键方面是大规模并行计算的使用。仔细处理这些计算资源对于开发它们的巨大潜力至关重要。将一个给定的问题划分为许多子问题，这些子问题可以有效地并行解决，这需要复杂的分割启发式和编码。不幸的是，今天这种启发式的发展主要依赖于关于这个问题的专家知识和明智的人工优化。这项研究为复杂启发式的自动化构建提供了进展，也改进了常用数学运算的编码。除了自动解决长期存在的开放问题外，研究还打算从解决方案中提取信息，以获得有用的数学见解。著名的数学挑战，如Collatz猜想和Hadwiger-Nelson问题，是推动这项工作的激励例子，它们可以帮助这项技术成为主流。研究人员将包括研究生和本科生。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

State-of-the-art automated theorem proving tools have been making progress on, and in some cases resolve, longstanding unsolved problems of mathematics like: can the positive integers be sorted into two buckets, so that neither bucket contains a Pythagorean triple (a solution to a^2+b^2=c^2), or can the points on the plane be colored 5 colors, so that every two points at distance 1 apart are colored differently? The same techniques are also crucial in industry to verify hardware and software. A key aspect of recent and future successes in mechanized mathematics is the use of massively parallel computation. Handling these computing resources carefully is vital to exploit their great potential. Sophisticated splitting heuristics and encodings are required to partition a given problem into many sub-problems that can be efficiently solved in parallel. Unfortunately, today the development of such heuristics depends predominantly on expert knowledge about this problem and on sensible manual optimization.This research offers advances towards automated construction of sophisticated heuristics, as well as improved encodings of commonly used mathematical operations. Apart from solving long-standing open problems automatically, the research intents to extract information from the solutions to acquire useful mathematical insights. Famous mathematical challenges like the Collatz conjecture and the Hadwiger-Nelson problem are motivating examples that are driving this work and they could help making this technology go mainstream. The investigators will involve both graduate and undergraduate students in this research.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.