Discovering concise scientific formulas that explain natural phenomena and align with existing theories is crucial. Traditional methods manipulate equations based on existing knowledge and experimental verification, but this process can be inefficient. This paper proposes AI-Hilbert, a novel approach that integrates experimental data and background knowledge (expressed as polynomials) into the discovery process. Using mixed-integer linear or semidefinite optimization, AI-Hilbert solves polynomial optimization problems and provides formal proofs of validity using Positivstellensatz certificates. The approach successfully derives famous scientific laws, such as Kepler's Law of Planetary Motion and the Radiated Gravitational Wave Power equation, demonstrating its potential to accelerate scientific discovery.

Ryan Cory-Wright, Cristina Cornelio, Sanjeeb Dash, Bachir El Khadir, Lior Horesh