The Gold Rush in AI4Math, II: What are signatures of AI-assisted Proofs?

Yuanchuan Guo; Jiashun Jin; Zheng Tracy Ke; Bingcheng Sui

cs.AINov 5, 2026

The Gold Rush in AI4Math, II: What are signatures of AI-assisted Proofs?

Authors: Yuanchuan Guo, Jiashun Jin, Zheng Tracy Ke, Bingcheng Sui

Abstract

The growing use of AI in mathematics raises a question: can we detect AI involvement in proofs, separately from AI assistance with writing? Historical arXiv papers, recent papers disclosing substantive AI use, and manuscripts released by OpenAI provide a rich empirical basis for studying this question. However, several challenges remain: lack of matched case-control pairs; potential incompleteness of disclosure; and lack of ready-to-use features designed to capture signals of AI involvement in proofs. To address these challenges, we construct five cohorts comprising 8,281 papers by combining existing manuscripts with those we produced using generative AI. These cohorts span different levels of AI involvement and include matched pairs of papers addressing the same research problems. We then introduce ProofTrace, a framework that represents each paper as a graph of immediate proof support (GIPS) and extracts interpretable features of mathematical organization. Our study yields three discoveries. First, principal-component projections of our features reveal a qualitative gradient of AI involvement, where AI-reworded papers remain close to human papers, the two AI-generated cohorts depart in broadly shared directions, and papers disclosing substantive AI use occupy intermediate positions which shifts toward AI-generated cohorts over time. Second, we identify recurring signatures of AI-generated proofs, such as fewer externally cited results, greater reliance on intermediate conclusions, and altered graph connectivity; many of these signatures persist under controls for research field, manuscript length, or graph size. Finally, in a separate detection experiment, ProofTrace distinguishes human-written papers from those disclosing substantive AI use. Its performance remains stable under AI rewording, whereas the performance of state-of-the-art text-based detectors declines sharply.

Figures & tables

Figure 1: (a) Five cohorts and study design. Sizes of the five cohorts and sampling of the Human cohort. (b) Two one-to-one pairing designs. Generation of the AI-rebuilt and AI-reworded papers from their Human sources.

Figure 2: A six-node subgraph of the GIPS excerpt from Wu et al. (2022) . Arrows show direct use; I40, I44, and I45 are within-proof conclusions. Features use the complete 77-node graph (Figure B1 ).

Family	Count	Example measurement	Example value
References	38	Cited-result nodes / all nodes	$3/77\approx 0.039$
Organization	82	Fraction of dependencies whose premise first appears later in the text	$8/77\approx 0.104$
Node Statistics	28	Intermediate conclusions / stated results	$64/13\approx 4.92$
Edge Statistics	86	Maximum in-degree / mean in-degree	$8/(77/77)=8$
Graph Motifs	34	Feed-forward triangles / directed two-step walks	$1/95\approx 0.011$
Global Topology	74	Nodes in the largest weakly connected component / all nodes	$53/77\approx 0.688$

Table 1: Six feature families, one example per family. The ‘Count’ column contains the total number of features in each family. The ‘Example value’ column is calculated on the extracted GIPS of Wu et al. (2022) .

Figure 3: Structural landscape of the five cohorts. (a,b) PC1–PC2 and PC1–PC3 projections. 8,281 papers on 342 structural features. Contours enclose approximately the densest half of each cohort, and larger dots show cohort means. (c) Relative positions of cohort means. Computed on the 285 features with a significant unpaired difference between Human ( $r=0$ ) and AI-rebuilt ( $r=1$ ). Dots and bars show medians and interquartile ranges.

Figure 4: Temporal positions of Hybrid papers from September 2025 to August 2026 relative to Human (

r=0

) and AI-rebuilt (

r=1

) reference means. Panels show (a) 265 structural and (b) 35 linguistic features with significant paired AI-rebuilt–Human differences. Solid lines: medians after adjusting period means for research field, reported AI-use group and revised-version status. Dashed lines: unadjusted medians. Shaded bands: interquartile ranges across features.

Figure 5: (a) Manhattan-style display of structural differences. Paired-test results for 700 paired Human and AI-rebuilt papers, by family. Evaluation metric: unadjusted $p$ -value, significant at Benjamini–Hochberg $q<0.05$ . (b) Significant features per family. Results for the 265 features with a significant mean difference and the 35 additional features that differ only in distribution.

Figure 6: Interpretations of twelve structural features in the paired Human–AI-rebuilt comparison. Each feature has largest or smallest standardized mean differences among significant features in the corresponding feature family.

Figure 7: Recurrence and robustness of structural features. Reference rows show 265 significant AI-rebuilt–Human features in (a) and 166 significant Hybrid–Human features restricted to six research fields in (b). Subsequent bars partition each reference set into significant features in the same direction (green), significant reversals (red), and insignificant features (gray). Blue features are outside the reference set and have a significant difference. Significance: Benjamini–Hochberg $q<0.05$ .

Pretrained and zero-shot baselines
	Original		Reworded
Method / variant	AUROC	AP	AUROC	AP
MELD (pretrained)	0.7904	0.7602	0.1618	0.3369
ModernBERT-MAGE (pretrained)	0.4513	0.4889	0.4149	0.4360
DETree (pretrained)	0.4220	0.4505	0.4183	0.4494
ToS (pretrained)	0.4128	0.4349	0.1930	0.3425

Table 2: Detection results of the two experiments for ProofTrace, ProofTrace++ and the other baselines. Evaluation metric: AUROC and AP with Hybrid as positive, higher is better.

Appendix figures & tables11 assets

Supplementary material from the paper’s appendix.

Appendix

Figure B1 : The complete GIPS of Wu et al. (2022) . We place each node vertically by the first recorded position of its statement and horizontally by the number of edges on the longest chain of dependencies that ends at it, with I37 and I38, which use each other, counted as one node. L, C, and T stand for lemmas, corollaries, and theorems, and I stands for intermediate conclusions.

Attribute	Content
id	The parser’s label of a stated result (e.g., Lemma 2.4, or U1, U2, … if it has no number). Intermediate conclusions are labeled I1, I2, and so on.
kind	stated if the result is explicitly stated as a theorem, lemma, proposition, corollary, claim, fact or observation. Otherwise intermediate .
statement_lines	For a stated result, where the parser finds its statement. For an intermediate conclusion, each sentence that asserts it, with its displays.
proof_lines	The ranges from where the paper starts to establish the conclusion to where it is established, including deferred parts. Empty if the paper gives no proof.
summary	For a stated result, its statement as the parser finds it. For an intermediate conclusion, the conclusion in at most two sentences.
evidence	One quotation. For a stated result, we quote from its proof. For an intermediate conclusion, we quote the clause that asserts it.

Appendix

Table B1 : The attributes of each node.

Attribute	Content
source	The identifier of the result used as a direct premise.
target	The identifier of another result whose written argument directly uses the conclusion of the source.
use_lines	The ranges where the target argument uses the premise.
evidence	One verbatim quotation where the target argument uses the premise.

Appendix

Table B2 : The attributes of each edge.

Attribute	Content
id	Corollary 2.2
kind	stated
summary	Corollary 2.2. Let $\mathbb{T}$ be an arbitrary time scale and $c$ be an arbitrary nonnegative constant. Then we have $\int_{a}^{b}\int_{a}^{t_{1}}\cdots\int_{a}^{t_{n-1}}c~\Delta t_{n}\cdots\Delta t_{1}\leq\frac{c(b-a)^{n}}{n!},$ where $a,b\in\mathbb{T},a\leq t_{n-1}\leq\cdots\leq t_{1}\leq b.$
evidence	2. Now suppose $k\leq n-1$ and that $S(k)$ holds. Then $\begin{split}&\int_{a}^{t_{n-(k+1)}}\cdots\int_{a}^{t_{n-1}}c~\Delta t_{n}\cdots\Delta t_{n-k}\\ \leq&\int_{a}^{t_{n-(k+1)}}\frac{c(t_{n-k}-a)^{k}}{k!}\Delta t_{n-k}\leq\int_{a}^{t_{n-(k+1)}}\frac{c(t_{n-k}-a)^{k}}{k!}\mathrm{d}t_{n-k}=\frac{c(t_{n-(k+1)}-a)^{k+1}}{(k+1)!}.\end{split}$ Thus, $S(k+1)$ holds.
id	I44
kind	intermediate

Appendix

Table B3 : The four nodes of the path Corollary 2.2

\to

I44

\to

I45

\to

Theorem 4.1, with text as in the article.

Feature	Human	AI-rebuilt	$d$	$q$
References
Externally cited-result fraction	0.061	0.002	$-1.39$	$4.1\times 10^{-103}$
Fraction of nodes that are externally cited results.
Cited-node fraction	0.061	0.002	$-1.38$	$1.4\times 10^{-102}$
Fraction of nodes that are cited.
Cited-to-uncited edge fraction	0.066	0.002	$-1.28$	$3.2\times 10^{-92}$

Appendix

Table C1 : The five structural features of each family with the largest

\lvert d\rvert

in the paired AI-rebuilt–Human comparison. Human and AI-rebuilt are the cohort means,

d

is the standardized mean difference, and

q

is the Benjamini–Hochberg adjusted

p

-value of the paired test.

Figure C1 : PC1–PC2, PC1–PC3 and PC2–PC3 projections of the papers in the length-matched landscape. Faint points are papers, contours enclose approximately the densest half of each cohort, and larger dots show cohort means. The panel titles give the between-cohort share

\sum_{c}n_{c}\lVert\bar{z}_{c}-\bar{z}\rVert^{2}/\sum_{i}\lVert z_{i}-\bar{z}\rVert^{2}

, where

z_{i}

is the point of paper

i

\bar{z}

the mean of all points, and

n_{c}

and

\bar{z}_{c}

the size and mean of cohort

c

. The number marked “outside” in each panel counts the papers beyond its displayed range.

Figure C3 : Six structural features in the five cohorts of the length-matched landscape, one from each family. Boxes show interquartile ranges, inner lines show medians, and whiskers reach the 5th and 95th percentiles.

Figure C4 : Change of each structural feature with posting date in Hybrid papers, against its paired AI-rebuilt–Human

d

. Panel (a) uses posting date alone, and panel (b) holds research field, reported AI-use group and revised-version status fixed. Each dot is one feature, colored by family. Filled dots are significant slopes, and a dot in the upper right or lower left quadrant changes in the direction of

d

Figure C5 : Classes of the structural features in the Hybrid–Human comparison. (a) Paired AI-rebuilt–Human

d

against Hybrid–Human

d

, by family. Green, red and gray features are in the reference set. Their Hybrid–Human difference is significant with the same sign (green), significant with the opposite sign (red) or not significant (gray). Blue features are outside the reference set and have a significant difference. Open circles are features significant in neither comparison. (b) Number of features in each class, by family.

Figure C6 : Classes of the structural features in the AI–Human comparison, drawn as in Figure C5 .

Figure C7 : Human and Hybrid papers of the training set by research field. The darker part of each bar counts the papers taken by matching on both research field and manuscript length.

Robustness of Machine-Generated Text Detection

Robustness of machine-generated text detection studies whether AI-text detectors remain reliable across shifts, edits, languages, and adversarial attacks.

See all 98 papers

Multimodal AI Detection for Math-Heavy Scientific Text
Oct 15, 2026Yixuan Huang, Danish Pruthi, Bhuwan DhingraAI-Generated Text Detection Robustness of Machine-Generated Text Detection
Duke University · Indian Institute of Science
Characterizing initial human-AI proof formalization workflows
Jun 2, 2026Katherine M. Collins, Simon Frieder, Jonas Bayer +14Human-in-the-Loop AI Autoformalization
Massachusetts Institute of Technology · University of Oxford · University of Cambridge +5
Artificial Intelligence for Mathematical Reasoning: An Integrated Survey of Language Models, Neuro-symbolic Systems, and Verified Discovery
Jun 7, 2026Syed Rifat Raiyan, Mohsinul Kabir, Hasan Mahmud +2Mathematical Reasoning Benchmarks Automated Theorem Proving
Systems and Software Lab (SSL), Department of Computer Science and Engineering, Islamic University of Technology, Gazipur, Bangladesh · Department of Computer Science, University of Manchester, Manchester, United Kingdom

Oct 15, 2026J/K move · Enter open · S save

Multimodal AI Detection for Math-Heavy Scientific Text

Yixuan Huang, Danish Pruthi, Bhuwan Dhingra

Duke University · Indian Institute of Science

AI-Generated Text Detection Robustness of Machine-Generated Text Detection

Open paper AskPDF arXiv

As large language models become increasingly capable of generating, and assisting with, scientific writing, there is a need for greater transparency and disclosure around the use of AI in research. Consequently, a veritable subfield of research and a number of commercial services aim to flag AI-generated content automatically. However, existing detectors which rely only on text extracted from PDFs fail to benefit from the rich visual information contained in the formatting of math-heavy scientific content. To study this, we select human-written proof and prose passages from pre-2022 arXiv LaTeX sources and re-generate them using 15 modern LLMs within the context of the same paper. This leaves us with coupled human and AI outputs in three different representations: the LaTeX source, a rendered image of the PDF, and the text extracted from the PDF. We find that the accuracy of the state-of-the-art Pangram 4 drops significantly as the mathematical content in a passage increases, especially when evaluated on text as opposed to LaTeX. However, this is not an inherent limitation of detecting AI-generated math: finetuning Qwen-3.5-27B based detectors on this domain recovers the gap, with LaTeX inputs performing significantly better than text since they preserve more formatting information. Since LaTeX sources are rarely available in practice, we also train SnapJudge: an image-based detector operating on screenshots of both prose and proofs from papers. At 0.1% false positive rate, SnapJudge achieves a detection rate of 92% on proofs and 93% on prose generated by frontier models, substantially outperforming both Pangram 4 and our text-based detector. We release our data, models and code at https://nlplab.cs.duke.edu/snapjudge.

Abstract

Robustness of Machine-Generated Text Detection

Explore similar work

Multimodal AI Detection for Math-Heavy Scientific Text

Characterizing initial human-AI proof formalization workflows

Artificial Intelligence for Mathematical Reasoning: An Integrated Survey of Language Models, Neuro-symbolic Systems, and Verified Discovery