Axiom-Aware FunSearch for Non-Constructive Mathematics

Evaluator-driven discovery systems (e.g., FunSearch) succeed when the target admits a clear fitness metric (e.g., “find the largest cap set”), but many central mathematical objects—Vitali sets, the Banach–Tarski paradox, Hamel bases, ultrafilters, etc.—lack such metrics and often rely on specific nonconstructive axioms, such as the axiom of choice (AC). We propose a FunSearch variant with a theorem proposer and a Lean-verified, axiom-aware evaluator that scores candidates by (i) proof progress, (ii) property coverage, and (iii) an axiom footprint that audits reliance on Choice (AC), Zorn’s Lemma, the axiom of dependent choice (DC), the law of excluded middle (EM), and others. A minimal prototype reconstructs proofs of the existence of a right inverse for an arbitrary surjection (via AC). We claim no new theorems, but provide early evidence that axiom-aware evaluation broadens evaluator-driven discovery beyond purely executable code.