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

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

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.