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

• URL: http://arxiv.org/abs/2604.17229v1
• Date: Sun, 19 Apr 2026 03:27:16 GMT
• Title: Yanasse: Finding New Proofs from Deep Vision's Analogies, Part 1
• Abstract summary: System extracts tactic usage distributions across 27 top-level areas of Mathlib.<n>It computes z-scores to identify tactics that are heavily used in a source area but rare or absent in a target area.<n>It matches source and target proof states via GPU-accelerated NP-hard analogy.
• Score: 51.56484100374058
• License: http://creativecommons.org/licenses/by-sa/4.0/
• 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 ω 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.

Related papers

• Game Hopping in Lean [5.623680633781937]
  We present HOPSCOTCH, a Lean 4 framework for mechanizing sound, game-based cryptographic proofs.<n>Security definitions are expressed as indistinguishability between stateful probabilistic oracles, and proofs follow the standard game-hopping paradigm.<n>We illustrate the framework with formalized proofs of the IND-CCA security of encrypt-then-MAC, the security of ElGamal encryption from DDH, the implication from one-time secrecy to public-key IND-CPA security, and the GGM pseudorandom-function construction.
  arXiv  Detail & Related papers  (2026-08-06T16:52:16Z)
• Geometric Measurements of the Axiom of Choice in Neural Proof Embeddings [0.2538209532048866]
  We use Lean 4's kernel-level tracking of axiom dependence to show that the axiom of choice has a measurable geometric correlate in proof space.<n>We show that the signature survives length, file, author, and topic controls, and replicates under full-source encoders trained on normalised proof source.
  arXiv  Detail & Related papers  (2026-06-26T19:57:00Z)
• LiveMathematicianBench: A Live Benchmark for Mathematician-Level Reasoning with Proof Sketches [61.30693283718321]
  We present LiveMathematicianBench, a dynamic multiple-choice benchmark for research-level mathematical reasoning.<n>By grounding evaluation in newly published theorems, it provides a realistic testbed beyond memorized patterns.<n>It employs a proof-sketchguided distractor pipeline that uses high-level proof strategies to construct plausible but invalid answer choices.
  arXiv  Detail & Related papers  (2026-04-02T08:22:17Z)
• Gödel's Poetry [0.0]
  We introduce a new approach to computer theorem proving, one that employs specialized language models for Lean4 proof generation.<n>We achieve a 90.4% pass rate on miniF2F without decomposition.<n>A key technical contribution lies in our extension of the Kimina Lean Server with abstract syntax tree (AST) parsing capabilities.
  arXiv  Detail & Related papers  (2025-12-16T10:00:01Z)
• BRIDGE: Building Representations In Domain Guided Program Verification [67.36686119518441]
  BRIDGE decomposes verification into three interconnected domains: Code, Specifications, and Proofs.<n>We show that this approach substantially improves both accuracy and efficiency beyond standard error feedback methods.
  arXiv  Detail & Related papers  (2025-11-26T06:39:19Z)
• Generative Logic: A New Computer Architecture for Deterministic Reasoning and Knowledge Generation [0.0]
  Generative Logic (GL) is a deterministic architecture that starts from usersupplied axiomatic definitions.<n>GL enumerates conjectures, applies normalization, type, and CE filter, and automatically reconstructs machine-checkable proofs.
  arXiv  Detail & Related papers  (2025-07-25T17:29:19Z)
• ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis [50.020850767257095]
  We propose ProofAug, a procedure that equips LLMs with automation methods at various granularities.<n>Our method is validated on the miniF2F benchmark using the open-source deep-math-7b-base model and the Isabelle proof assistant.<n>We also implement a Lean 4 version of ProofAug that can improve the pass@1 performance of Kimina-Prover-seek-Distill-1.5B from 44.3% to 50.4%.
  arXiv  Detail & Related papers  (2025-01-30T12:37:06Z)
• Proving Theorems Recursively [80.42431358105482]
  We propose POETRY, which proves theorems in a level-by-level manner. Unlike previous step-by-step methods, POETRY searches for a sketch of the proof at each level. We observe a substantial increase in the maximum proof length found by POETRY, from 10 to 26.
  arXiv  Detail & Related papers  (2024-05-23T10:35:08Z)
• Enhancing Neural Theorem Proving through Data Augmentation and Dynamic Sampling Method [1.8130068086063336]
  We introduce DS-Prover, a novel dynamic sampling method for theorem proving. We augment the training dataset by decomposing simplification and rewrite tactics with multiple premises into tactics with single premises. We achieve a state-of-the-art performance (Pass@1) of 14.2% on the ProofNet dataset and a performance of 29.8% on MiniF2F.
  arXiv  Detail & Related papers  (2023-12-20T09:55:21Z)
• LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Provers [60.009969929857704]
  Logical reasoning is an important task for artificial intelligence with potential impacts on science, mathematics, and society. In this work, we reformulating such tasks as modular neurosymbolic programming, which we call LINC. We observe significant performance gains on FOLIO and a balanced subset of ProofWriter for three different models in nearly all experimental conditions we evaluate.
  arXiv  Detail & Related papers  (2023-10-23T17:58:40Z)
• A Theory of Label Propagation for Subpopulation Shift [61.408438422417326]
  We propose a provably effective framework for domain adaptation based on label propagation. We obtain end-to-end finite-sample guarantees on the entire algorithm. We extend our theoretical framework to a more general setting of source-to-target transfer based on a third unlabeled dataset.
  arXiv  Detail & Related papers  (2021-02-22T17:27:47Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.