Yanasse: Finding New Proofs from Deep Vision's Analogies, Part 1

TL;DR

Yanasse introduces a domain-independent method leveraging deep vision and analogy to transfer proof strategies across mathematical areas, successfully generating new proofs in Lean with high accuracy.

Contribution

The paper presents a novel, domain-agnostic approach combining deep vision, analogy, and AI reasoning to discover new mathematical proofs by transferring tactic patterns.

Findings

Produced 4 verified proofs out of 10 attempts (40%) in probability to representation theory transfer.

Tactic schemas decompose into a head and a modifier, with the modifier often transferring across domains.

The matching engine is domain-independent, relying only on a relation extractor.

Abstract

Project Yanasse presents a method for discovering new proofs of theorems in one area of mathematics by transferring proof strategy patterns (e.g., Lean 4 tactic invocation patterns) from a structurally distant area. The system extracts tactic usage distributions across 27 top-level areas of Mathlib (217,133 proof states), computes z-scores to identify tactics that are heavily used in a source area but rare or absent in a target area, matches source and target proof states via GPU-accelerated NP-hard analogy (running on a MacBook Air via Apple's MPS backend), and then asks an AI reasoning agent to semantically adapt--not symbol-substitute--the source tactics invocation pattern to the target theorem. In this first part of the study, the method is applied to the pair Probability -> Representation Theory, producing 4 Lean-verified new proofs out of 10 attempts (40%). The proofs compile with zero sorry declarations. The key finding is that tactic schemas decompose into a head (domain-gated, rarely transfers) and a modifier (domain-general, often transfers): filter upwards's head fails in representation theory (no Filter structure), but its [LIST] with {\omega} modifier transfers cleanly as ext1 + simp [LIST] + rfl. Crucially, the underlying matching engine--deep vision lib.py--is entirely domain independent: the same optimization code for an NP-hard matching that matches chess positions by analogy matches Lean proof states by analogy, without knowing which domain it is processing. Only a relation extractor is domain-specific.