AI RESEARCH

OpenAI's math repo holds hundreds of model-written manuscripts, some with Lean proofs. What Lean verifies, what it misses, and the lesson for agent output.

Anthropic's Lean formalization of Fermat's Last Theorem, read for developers: what Claude verified in 11 days and the repo patterns worth copying.

ASR benchmark optimization, quantified: a Hume AI and Hugging Face study finds 6 of 11 speech models reproduce benchmark transcripts instead of the audio.

ICML 2026 reproduction audit: coding agents checked 2,226 papers claim by claim, and 23% had a falsified or contested claim. What the challenge found.

CLAUDE.md and AGENTS.md files keep growing because the reasoning behind each rule decays. A study of 1,867 repos names the mechanism and a comment-based fix.

EvoX Genesis built a Rust C compiler for $44 in tokens by keeping the project persistent and agents finite-lived. What the design says about agent memory.

OpenAI's Astra model produced results on ten decade-old math problems, including Erdős problems, each with a Lean 4 certificate. What shipped and why.

AGENTS.md and CLAUDE.md configuration smells: a SCAM 2026 study of 100 top repos catalogs six, led by Lint Leakage and Context Bloat. What to fix in yours.

Coding agents rarely read open source AI contribution rules on their own and never refuse AI-banned repos. RepoComplianceBench shows what prompts can fix.

AGENTS.md and context files do not measurably change coding agent correctness in a 288-run Claude Code and Codex ablation. Failures were implementation skill.

LLM agents resolve real Java merge conflicts more often than structured merge tools in a calibrated ConflictBench study. Their edge is coverage: tools abstain.

Kimi Linear explained: Moonshot's KDA hybrid linear attention beat full attention with 75% less KV cache and up to 6x faster decoding at 1M context.

GPT-5.6 helped produce a Lean-verified proof closing a 1996 gap in derivative-free convex optimization. How the 10-page expert prompt worked, and what HN said.

GPT-5.6 Sol Ultra proof of the Cycle Double Cover Conjecture: what OpenAI claims, the prompt it used, and why mathematicians are still verifying the result.

Anthropic's new research reveals LLMs have an internal 'workspace' for silent reasoning - and it could change how we build safer AI.

Leanstral 1.5 is Mistral's open Apache-2.0 model for Lean 4 theorem proving. The benchmark claims, the HN pushback on its bug-finding pitch, and how to use it.

VibeThinker-3B is a 3B parameter reasoning model reporting 94.3% on AIME 2026. What the paper claims, how to run it locally, and what it trades away.