On Radically Expanding the Landscape of Potential Applications for Automated Proof Methods

Abstract

In this paper we examine the potential of computer-assisted proof methods to be applied much more broadly than commonly recognized. More specifically, we contend that there are vast opportunities to derive useful mathematical results and properties that are extremely narrow in scope, and of practical relevance only to highly-specialized engineering applications, that are presently overlooked because they have characteristics atypical of those that are conventionally pursued in the areas of pure and applied mathematics. As a concrete example, we demonstrate use of automated methods for certifying polynomial nonnegativity as a part of a dimension-pinning strategy to prove that the inverse of the relative gain array (RGA) of a d-dimensional positive-definite matrix is doubly-stochastic for $d\le 4$.

Expanded narrative

References in corpus (7)

• N=6 superconformal Chern-Simons-matter theories, M2-branes and their gravity duals
• Sparsity-Cognizant Total Least-Squares for Perturbed Compressive Sampling
• Towards an M5-Brane Model I: A 6d Superconformal Field Theory
• On the Relative Gain Array (RGA) with Singular and Rectangular Matrices
• Geometric Langlands From Six Dimensions
• Sign Patterns of Inverse Doubly-Nonnegative Matrices
• Expression of a Real Matrix as a Difference of a Matrix and its Transpose Inverse