Beyond Correctness: Toward Automated Novelty Verification with Lean 4

ProofJudge: Tool-Grounded LLM Evaluation of Formal Proof Quality in Mathlib

Formal proofs in Lean 4 that pass the kernel's type checker can nonetheless vary widely in quality. We introduce ProofJudge, an agentic LLM-as-judge system that scores formal proof quality along five dimensions beyond correctness: library leverage, automation fit, structural clarity, statement quality, and Mathlib conventions. We evaluate ProofJudge on a novel dataset of 218 declarations drawn from distinct Mathlib PRs. The judge agent is grounded by tool access to the commit the PR is applied to, enabling it to query the library state when scoring. A judge is considered aligned with human preferences when it rates the version of the PR Mathlib accepted above the initial version that was sent back for revision. All six judge models evaluated recover the reviewers'preference well above chance, from 80.8% to 63.5%, and two open-weight judges reach roughly 70% at a tenth of the best judge's cost. We release the judge harness, evaluation dataset, and evaluation traces as open-source artifacts to support further research.

Neuro-Formal Verification: Agentic Language-Agnostic Formal Program Reasoning

Neuro-formal verification is introduced, which harnesses that automation for developers of mainstream programming languages and returns a Dafny proof of correctness or of a bug on 57% of the entries at 92% precision, and a CBMC counterexample for 63% of the buggy programs at 90% precision.

ITPEval: Benchmarking Formal Translation Across Interactive Theorem Provers

ITPEval is presented, the first benchmark for evaluating automated formal proof translation across four major ITPs (Lean 4, Rocq, Isabelle, and HOL Light), spanning two distinct logical foundations and itpeval, a unified multi-ITP verification infrastructure with state-isolated warm backends that preserve per-artifact native checking semantics.

Library Before Proof: Making LLM-Generated Rocq Usable by Mathematicians

MathAdv: What Theorem Provers Know, Reason, Formalize, and Generalize

Formal theorem proving enables machine-verifiable evaluation of mathematical reasoning, yet existing benchmarks often emphasize aggregate proof accuracy, concentrate on a narrow range of mathematics, and provide limited evidence of robustness to equivalent reformulations. We introduce MathAdv, a diagnostic benchmark spanning 13 domains across undergraduate- and graduate-level mathematics. Alongside Lean 4 theorem proving, MathAdv provides up to three auxiliary tasks: multiple-choice questions that probe mathematical knowledge, fill-in-the-blank problems that isolate informal reasoning, and expert-crafted transformations that test robustness to problem presentation. Our evaluation of contemporary theorem provers yields four findings: formalization remains a major bottleneck; performance varies substantially across mathematical domains; natural-language guidance helps general-purpose LLMs but can hinder proof-specialized models; and mathematically equivalent reformulations expose substantial robustness limitations. Together, these results show how component-wise evaluation can reveal model capabilities and failure modes that aggregate theorem-proving accuracy obscures. The dataset and evaluation scripts are available at https://github.com/margotyjx/MathAdv.git.

When Logical Correctness Is Not Rational Judgment: The Limits of Formal Reasoning in Algorithmic Decision Systems

Algorithmic failures are conventionally diagnosed as deviations from a correct specification — bias to be corrected, error to be patched. This article argues that the more consequential and less visible failure mode runs the other way: a system executes its specification exactly, and the specification was inadequate to the situation it governed. The distinction is developed through a formal argument rather than an analogy. Treating the feature set available to a learning system as a -algebra , the article shows that no -measurable function can represent a value-relevant event excluded from , and — more precisely — that no -measurable self-assessment functional can take the adequacy of  itself as an argument. Every reliability measure a model reports, from calibration to conformal coverage, is computed inside the representation whose adequacy is in question. Sections 2 and 3 locate this claim against the literatures on bounded rationality, rule-following, and algorithmic fairness, arguing that each stops short of the reflexive point at issue. Sections 4 through 6 develop the argument through decision theory, the Rashomon set, Goodhart-type selection effects, and an impossibility theorem for fairness criteria, and confront the two strongest objections available — that scope-monitoring is already being formalised, and that closure under a fixed representation cannot be a principled limit if human reasoners are themselves physical systems. The article concludes that formal validity and practical rationality answer to different criteria of success, that the empirical superiority of statistical prediction over human judgment does not collapse this distinction, and that the operative difference lies in the structure of failure rather than in its frequency: formal errors are quiet, mechanically correlated, and reproduced at scale, while human error — correlated though it often is by institutional bias, professional norms, and bureaucratic routine — remains comparatively noisy, locally visible, and costly to scale.