Back to artifacts

AI for Science: January 2026 Week 3

Jan 12 – Jan 18, 2026 · 42 papers analyzed · 3 breakthroughs

Summary

Analyzed 42 unique papers from Jan 12-18 2026 across AI4Math, AI4Physics, and Scientific ML. 3 breakthroughs: (1) 2601.10791 OmniMol transfers particle physics foundation model to molecular dynamics, achieving competitive MLIPs with 20x fewer parameters; (2) 2601.07953 introduces quantum automated theorem proving framework with quadratic speedup for propositional, first-order, and geometric reasoning; (3) 2601.07421 resolves Erdos Problem #728 via AI-human collaboration, first Erdos problem fully solved autonomously with Lean proof. Key trends: cross-domain foundation models emerging in scientific ML, quantum computing expanding into formal reasoning, neuro-symbolic approaches maturing for software verification.

Key Takeaway

Week 3 of 2026 marks milestones in AI-for-Science cross-pollination: particle physics models transfer to molecular dynamics, quantum computing enters theorem proving, and the first Erdos problem falls to AI-assisted formal proof. The unifying theme is integration - combining pre-trained models across domains, merging neural flexibility with symbolic rigor, and blending human insight with machine verification.

Breakthroughs (3)

1. OmniMol: Transferring Particle Physics Knowledge to Molecular Dynamics with Point-Edge Transformers

Why Novel: First successful cross-domain transfer from high-energy physics to molecular dynamics, demonstrating that a transformer foundation model pre-trained on 1 billion particle jets can be adapted for machine-learned interatomic potentials with strong low-data performance and ~20x fewer parameters than domain-specific baselines.

Key Innovations:

  • Adapts OmniLearn, a Point-Edge Transformer pre-trained on particle jets from the LHC, to molecular dynamics via physics-informed attention bias and domain-specific local features
  • Introduces interaction-matrix attention bias that injects pairwise atomic physics directly into transformer attention logits
  • Demonstrates strong few-shot learning: LoRA fine-tuning with just 10K-100K molecules achieves competitive performance
  • OmniMol-medium (43.3M params) achieves 1.34 meV/atom energy MAE, comparable to eSEN-medium (50.7M) at 1.32 meV/atom

Evidence:

  • — Comparison showing OmniMol-medium achieves competitive performance with 20x fewer parameters than Transformer-1B
  • — Scaling behavior demonstrating pre-training benefits especially in low-data regimes (10K-100K molecules)
  • — Model scaling comparison showing OmniMol matches eSEN performance trajectory with smaller architectures

Impact: Establishes cross-domain foundation model transfer as viable for scientific ML, opening pathways to leverage large pre-trained models from data-rich domains (particle physics, astronomy) for data-scarce scientific applications.

2. Quantum automated theorem proving

Why Novel: First comprehensive framework for quantum automated theorem proving, extending classical resolution and Wu's algebraic method to quantum computers with provable quadratic query complexity improvements for propositional logic, first-order logic, and geometric theorems.

Key Innovations:

  • Develops quantum resolution for propositional and first-order logic with quadratic reduction in query complexity via amplitude amplification
  • Extends Wu's algebraic method for geometric ATP to quantum setting using circuit-based polynomial pseudo-division and Kravchuk-based interpolation
  • Provides both state-based and circuit-based formulations with complete complexity analysis including polynomial identity testing on quantum computers
  • Demonstrates end-to-end quantum proof of IMO 2008 Geometry Problem 1 requiring circuits with up to 28 qubits and depth 89

Evidence:

  • — Overview of QATP framework showing knowledge base encoding and quantum reasoning for both logic and geometric problems
  • — Complete worked example of quantum pseudo-division for IMO geometry problem with circuit constructions

Impact: Bridges quantum computing and symbolic AI, establishing theoretical foundations for future quantum-assisted formal verification and mathematical reasoning systems with potential applications in formal methods and proof automation.

3. Resolution of Erdos Problem #728: a writeup of Aristotle's Lean proof

Why Novel: First Erdos problem regarded as fully resolved autonomously by an AI system (GPT-5.2 Pro + Harmonic Aristotle), producing a machine-verified Lean proof of a logarithmic-gap phenomenon for factorial divisibility that had remained open for decades.

Key Innovations:

  • Proves infinitely many triples (a,b,n) exist with a!b! | n!(a+b-n)! and C_1 log n < a+b-n < C_2 log n for any constants 0<C_1<C_2
  • Reduces problem to binomial divisibility and uses Kummer's theorem to translate p-adic valuations into base-p carry counts
  • Develops probabilistic counting argument with Chernoff bounds to find 'carry-rich but spike-free' integers m in each scale [M,2M]
  • Complete formalization in Lean with detailed correspondence between informal proof and formal development

Evidence:

  • — Main theorem statement: logarithmic gap window for factorial divisibility
  • — Key lemma establishing existence of good m with sufficient carries and bounded spikes for all primes p <= 2k

Impact: Landmark demonstration of AI-assisted mathematical discovery, showing that frontier LLMs combined with formal verification can resolve previously open problems, establishing a new paradigm for human-AI collaboration in mathematics research.

Trends

  • Cross-domain foundation model transfer: OmniMol demonstrates that physics knowledge learned from particle jets can transfer to molecular dynamics, suggesting cross-domain pre-training may unlock scientific ML where domain-specific data is limited.

  • Quantum computing meets formal reasoning: Quantum ATP framework and quantum ML for materials science show quantum advantage being explored beyond optimization into symbolic reasoning and active learning domains.

  • Neuro-symbolic integration maturing: CodeLogician and DiSOL demonstrate complementary strengths of neural and symbolic approaches, with LLMs handling translation/abstraction and formal methods providing rigor.

  • Hessian-aware training for physical properties: PFT shows that directly supervising second-order derivatives (Hessians) significantly improves prediction of vibrational and thermal properties beyond what energy/force training achieves.

  • AI-human collaboration in mathematics: Erdos #728 resolution establishes a new paradigm where AI systems propose solutions that humans verify and formalize, potentially accelerating progress on long-standing open problems.

Notable Papers (7)

1. Stability and Vibrations of Proteins in Vacuum and Water: Bridging Quantum Accuracy and Force-Field Efficiency

Demonstrates SO3LR MLFF reproduces PBE0+MBD DFT for biomolecular vibrations with unprecedented fidelity across small molecules to protein tetramers, achieving quantum accuracy at force-field cost.

2. PFT: Phonon Fine-tuning for Machine Learned Interatomic Potentials

Introduces Hessian-aware fine-tuning for MLIPs that directly supervises second-order force constants, achieving 55% improvement on phonon properties and state-of-the-art thermal conductivity predictions.

3. Imandra CodeLogician: Neuro-Symbolic Reasoning for Precise Analysis of Software Logic

Presents neurosymbolic agent integrating LLMs with ImandraX formal reasoner, closing 41-47 percentage point gap in software logic reasoning accuracy via formal model construction.

4. Discrete Solution Operator Learning for Geometry-Dependent PDEs

Introduces DiSOL framework learning discrete solution procedures rather than continuous operators, enabling stable predictions under topological changes and strongly OOD geometries.

5. CompNO: A Novel Foundation Model approach for solving Partial Differential Equations

Develops compositional neural operators with reusable Foundation Blocks for elementary differential operators, achieving lower L2 error than FNO/DeepONet with exact boundary condition enforcement.

6. Machine learning nonequilibrium phase transitions in charge-density wave insulators

Develops ML force-field for non-equilibrium electronic forces in driven Holstein model, reproducing CDW-to-metal phase transition dynamics with orders of magnitude speedup over NEGF.

7. Forcing and Diagnosing Failure Modes of Fourier Neural Operators Across Diverse PDE Families

Systematic stress-testing framework across 1000 FNO models and 5 PDE families, producing failure-mode atlas showing order-of-magnitude error inflation under distribution shifts.

Honorable Mentions

  • DataScribe: An AI-Native, Policy-Aligned Web Platform for Multi-Objective Materials Design and Discovery ()
  • Introduction to optimization methods for training SciML models ()
  • Physics-informed neural networks for angular-momentum conservation in computational relativistic spin hydrodynamics ()
  • Formalization of Amicable Numbers Theory ()
  • Shape-morphing programming of soft materials on complex geometries via neural operator ()
  • Physics-embedded neural computational electron microscopy for quantitative 4D nanometrology ()
  • Agentic AI and Machine Learning for Accelerated Materials Discovery and Applications ()
  • Quantum Kernel Machine Learning for Autonomous Materials Science ()