AI for Science: January 2026 Week 1

1. SeedFold: Scaling Biomolecular Structure Prediction

arXiv:2512.24354

Why Novel: Identifies width scaling as the key bottleneck for folding models and introduces linear triangular attention that reduces complexity from $O(N^3)$ to enable efficient scaling, combined with large-scale distillation to 26.5M samples.

Key Innovations:

• Discovers that Pairformer width (pair representation dimension) is the primary scaling bottleneck, not depth
• Introduces Gated Linear Triangular Attention reducing memory and compute while maintaining accuracy
• Constructs 26.5M sample distillation dataset from AFDB and MGnify for training data augmentation
• Achieves state-of-the-art on FoldBench, outperforming AlphaFold3 on protein monomers (0.889 vs 0.88 lDDT), antibody-antigen (53.2% vs 47.9% DockQ), and protein-RNA (65.3% vs 62.3% DockQ)

Evidence:

• tab:1 — Model configurations showing width/depth scaling strategies across Small/Medium/Large variants
• tab:3 — FoldBench results showing SeedFold outperforming AlphaFold3 on 5 of 8 tasks
• fig:2 — Scaling comparison demonstrating width scaling consistently outperforms depth scaling
• fig:3 — LinearTriangularAttention architecture with memory and time benchmarks showing 2-4x improvement
• fig:4 — Cumulative success rate distributions across interface modalities

Impact: Establishes a new state-of-the-art for open biomolecular structure prediction, providing both algorithmic insights (width > depth) and practical innovations (linear attention) that will influence future foundation model development.

2. LeanCat: A Benchmark Suite for Formal Category Theory in Lean (Part I: 1-Categories)

arXiv:2512.24796

Why Novel: First formal theorem proving benchmark specifically targeting category theory — the interface language of modern mathematics — exposing that current LLMs completely fail at abstraction-heavy, library-grounded reasoning (best model achieves only 12% pass@4 on full benchmark).

Key Innovations:

• Creates 100 category-theory problems formalized in Lean 4 (mathlib 4.19.0) spanning 8 thematic clusters from basic properties to monads
• Develops difficulty annotation pipeline combining model-based estimates and expert judgment for Easy/Medium/High classification (20/42/38 split)
• Benchmarks state-of-the-art models (Claude 4.5, GPT-5.2, Gemini 3 Pro, DeepSeek V3.2, Kimi K2) revealing stark performance gap: Claude 4.5 best at 8.25% pass@1 / 12% pass@4
• Quantifies natural-to-formal gap: models perform significantly better on natural language arguments than generating compilable Lean code

Evidence:

• tab:1 — Full benchmark results: Claude-opus-4-5 achieves 32.5%/50% on Easy but 0%/0% on High difficulty
• fig:1 — Formal proof accuracy (pass@4) visualization across model baselines
• fig:2 — Natural language vs formal language accuracy comparison highlighting the NL-to-FL bottleneck
• sec:1 — Introduction describing the abstraction gap in current benchmarks and LeanCat's design philosophy

Impact: Reveals a critical capability gap in LLM reasoning for abstract mathematics, establishing category theory as a frontier challenge and providing a rigorous benchmark for measuring progress toward genuine mathematical understanding.

3. Geometry of Reason: Spectral Signatures of Valid Mathematical Reasoning

arXiv:2601.00791

Why Novel: Introduces a training-free method for detecting valid mathematical reasoning via spectral analysis of attention patterns, achieving 82.8-85.9% accuracy without any task-specific training and discovering 'Platonic validity' — the ability to detect logically correct proofs that formal systems reject due to technical failures.

Key Innovations:

• Treats attention matrices as dynamic graphs and applies spectral diagnostics (Fiedler value, High-Frequency Energy Ratio, smoothness, spectral entropy) to detect reasoning coherence
• Achieves cross-architecture universality across 7 models from 4 families (Meta, Alibaba, Microsoft, Mistral) with effect sizes $|d| \geq 2.09$ and $p < 10^{-47}$
• Discovers 'Platonic validity': spectral method identifies mathematically valid proofs that Lean rejects due to timeout, imports, or formatting — detecting logical correctness rather than syntactic acceptance
• Identifies architectural dependency: Sliding Window Attention models require different spectral metrics (late-layer Smoothness vs HFER)

Evidence:

• sec:1 — Introduction presenting the epistemological challenge and spectral hypothesis grounded in graph signal processing
• fig:1 — Overview of spectral analysis pipeline from attention matrices to diagnostic metrics
• sec:experiments — 82.8-85.9% accuracy under nested cross-validation, up to 95.6% with calibrated thresholds
• sec:analysis:platonic — Analysis of Platonic validity phenomenon detecting correct proofs rejected by formal systems

Impact: Provides a fundamentally new approach to reasoning verification that complements formal proof assistants, offering interpretable signals about model 'epistemic state' and potentially enabling better reasoning-time interventions.

1. AceFF: A State-of-the-Art Machine Learning Potential for Small Molecules

arXiv:2601.00581

Introduces TensorNet2 with neutral charge equilibration for drug discovery MLIPs, achieving 1.76 kcal/mol MAE on Wiggle150 benchmark with 100+ ns/day simulation speeds.

2. Ab Initio Melting Properties of Water and Ice from Machine Learning Potentials

arXiv:2512.23939

Comprehensive benchmark of Deep Potential MLPs trained on MB-pol and DFT functionals for water melting properties, rigorously assessing nuclear quantum effects via PIMD.

3. Learning Density Functionals to Bridge Particle and Continuum Scales

arXiv:2512.23840

Augments classical density functional theory with neural corrections via adjoint optimization, accurately predicting LJ fluid contact angles and droplet shapes beyond training regime.

4. Expanding the Chaos: Neural Operator for Stochastic (Partial) Differential Equations

arXiv:2601.01021

Develops Wiener Chaos Expansion-based neural operators for SPDEs/SDEs, enabling one-shot trajectory reconstruction with theoretical guarantees across Navier-Stokes, diffusion sampling, and flood prediction.

5. Melting curve of correlated iron at Earth's core conditions from machine-learned DFT+DMFT

arXiv:2512.25061

Develops ML accelerator for DFT+DMFT achieving 2-4x speedup, predicting iron melting temperature of 6225 K at 330 GPa inner-core boundary pressure.

6. Constructing a Neuro-Symbolic Mathematician from First Principles

arXiv:2601.00125

Proposes Mathesis architecture encoding math as hypergraphs with differentiable Symbolic Reasoning Kernel providing dense gradient feedback for proof search.

7. Spectral Analysis of Hard-Constraint PINNs: The Spatial Modulation Mechanism of Boundary Functions

arXiv:2512.23295

Provides theoretical analysis of how boundary functions in hard-constraint PINNs modulate spectral properties, explaining when HC-PINNs outperform soft constraints.