Algorithm-Supported Mathematical Theory Exploration: A Personal View and Strategy

摘要

We present a personal view and strategy for algorithm-supported mathematical theory exploration and draw some conclusions for the desirable functionality of future mathematical software systems. The main points of emphasis are: The use of schemes for bottom-up mathematical invention, the algorithmic generation of conjectures from failing proofs for top-down mathematical invention, and the possibility to program new reasoners within the logic on which the reasoners work ("meta-programming").