2 papers
cs.AI2026
Yanasse: Finding New Proofs from Deep Vision's Analogies, Part 1
Alexandre Linhares
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…
cs.LO2026
Deep Vision: A Formal Proof of Wolstenholmes Theorem in Lean 4
Alexandre Linhares
We present a formal verification of Wolstenholme's theorem -- for prime -- in Lean~4 with Mathlib. The proof proceeds by expanding th…