Proofs by example

TL;DR

This paper explores the proof by example method for algebraic identities, proposing a practical approach to construct generic examples using advanced number theory tools, enabling efficient and approximate verification.

Contribution

It introduces a novel method leveraging diophantine geometry to construct generic examples for proof by example, with applications to plane geometry theorems.

Findings

Develops a framework for constructing generic examples using diophantine geometry.

Provides an effective inequality for algebraic varieties to facilitate approximate verification.

Demonstrates the approach with applications to geometric theorems.

Abstract

We study the proof scheme "proof by example" in which a general statement can be proved by verifying it for a single example. This strategy can indeed work if the statement in question is an algebraic identity and the example is "generic". This article addresses the problem of constructing a practical example, which is sufficiently generic, for which the statement can be verified efficiently, and which even allows for a numerical margin of error. Our method is based on diophantine geometry, in particular an arithmetic B\'ezout theorem, an arithmetic Nullstellensatz, and a new effective Liouville-Lojasiewicz type inequality for algebraic varieties. As an application we discuss theorems from plane geometry and how to prove them by example.