A machine-checked proof of the Dong-Yang classification of optimal (n,4) binary codes for BSCs

The purpose of this paper is two-fold. First, we show that, after a specified form isometry, the two-coordinate reduction in the binary Hilbert-symbol realization of Chinburg and Zhang is inverse to Kim's building-up construction, up to permutation equivalence. Second, for $q\equiv1\pmod4$, we develop a $q$-ary analogue of this reduction-and-extension mechanism. The identity $c^2=-1$ yields the isotropic line governing the split construction. For every fixed ordered pairing of the coordinates, we obtain a universal rank-$r$ boxed normal form, where $r$ is the dimension of the intersection with the product of these isotropic lines. Applications include optimal self-dual $[6,3,4]$ and $[8,4,4]$ codes over $\mathbb F_{5}$, optimal self-dual $[8,4,5]$ and $[10,5,6]$ codes over $\mathbb F_{13}$, and a self-dual $[12,6,6]$ code over $\mathbb F_{13}$. We also give an exact repeated boxed realization of self-dual $[18,9,8]$ and $[20,10,10]$ codes over $\mathbb F_{13}$, in which the split-boxed parent and its building-up child occur in one complete generator matrix. The algebraic core is formalized in Lean 4.

Lean 4 autoformalization has become increasingly popular in recent years, with frontier language models and open-weight autoformalizers now producing valid formalizations of mathematical theorems. However, these evaluations often rely on single canonical phrasings of theorems and rarely probe whether outputs are robust to natural variation in inputs, while prior work has shown that semantically equivalent paraphrases often induce divergent formal outputs. We study the structure of these divergences in Lean 4 by applying deterministic paraphrase rules to datasets of undergraduate and Olympiad-level math problems. Across four frontier models and three open-weight autoformalizers, we find that paraphrase sensitivity is dominated by failures at the code-generation layer, and that these failures are typed differently by dataset. Furthermore, these patterns generalize to open-weight models, showing that state-of-the-art autoformalizers still struggle to generate valid Lean code. Our results provide a failure-mode taxonomy for autoformalization and motivate training-time interventions targeted at specific compilation failures.

Within the past few years, the ability of Large Language Models (LLMs) to generate formal mathematical proofs has improved drastically. We provide a comparison of various LLMs' effectiveness in producing formal proofs in Lean 4 with the goal of assisting those seeking to use LLMs to support their own projects. We utilize both pass@$k$ and refine@$k$ metrics as the benchmark for our comparison and evaluate on subsets of both miniF2F and miniCTX datasets. Our testing shows that overall, Gemini 3.1 Pro and Claude Opus 4.7 perform best. Gemini 3.1 Pro achieved a 92% success rate on miniF2F via refine@32 whereas Opus 4.7 achieved a 86% success rate on miniCTX via refine@32. When taking cost into account, NVIDIA Nemotron 3 Super and GPT-OSS 120B were the most efficient, with competitive accuracies and average costs of <\0.01$ per correct proof.