Beyond Correctness: Toward Automated Novelty Verification with Lean 4

Ayrton Porto

Artificial intelligence systems applied to mathematics verify correctness but not novelty: an automatically generated theorem can compile in Lean without errors and yet be an alrea…