Papers With

← All papers
First page of On the asymptotic Makar-Limanov rank conjecture

On the asymptotic Makar-Limanov rank conjecture

SiZhuo Yan, Hao Shen, Jianting Yang

math.RA Oct 5, 2026 · v2
formalization mathlib algebra ai-agents
Read PDF arXiv abstract Code
TL;DR
The main theorem, the asymptotic Makar-Limanov rank conjecture, is formalized in Lean 4 with Mathlib, sorry-free and using only standard axioms, with a public repository.
Abstract
Let $\Bbbk$ be an algebraically closed field of characteristic zero and let $f$ be a nonconstant polynomial in finitely many freely noncommuting variables. We prove the asymptotic Makar-Limanov rank conjecture, namely that the normalized rank of a value of $f$ can be made arbitrarily small by choosing matrices over $\Bbbk$ of finite size.
Problem

Over an algebraically closed field of characteristic zero, a nonconstant free noncommutative polynomial need not have an exact zero matrix value. The asymptotic Makar-Limanov rank conjecture asks whether the normalized rank of its matrix values can nevertheless be made arbitrarily small.

Approach

The problem is first reduced to two generators via the substitution x_i ↦ xy^i. A symbol algebra of formal series with commuting derivations is then constructed, and a finite Newton approximation solves the resulting differential equations with inequations. These symbols are realized as matrices and compressed to finite matrices, and a Nullstellensatz-style argument descends the result back to the base field. The theorem is formalized in Lean 4 with Mathlib, with assistance from an AI agent system (MechMath Agent Team).

Results

The conjecture is proved: the infimum over n of minRank(f,n)/n equals 0 for every nonconstant free polynomial f. The Lean formalization of the main theorem contains no sorry and uses only the axioms propext, Classical.choice and Quot.sound.