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

## TL;DR

This paper explores the broader potential of computer-assisted proof methods, highlighting their ability to derive narrow, practically relevant mathematical results in specialized engineering contexts that are often overlooked.

## Contribution

It demonstrates how automated proof techniques can be applied to niche problems like certifying polynomial nonnegativity in control theory, expanding their scope beyond traditional mathematical domains.

## Key findings

- Automated methods can certify polynomial nonnegativity in specific engineering problems.
- Proof of inverse RGA properties for positive-definite matrices up to dimension 4.
- Broader applicability of proof methods to specialized, practical mathematical results.

## 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\leq 4$.