paper / jasondeanlee / Jun 7
LeanMarathon addresses a fundamental scaling failure in long-horizon autoformalization: not just proof difficulty, but context decay, statement drift, and dependency tangling across large Lean developments. The system introduces an "evolving blueprint" — a shared Lean file acting as formal skeleton, natural-language proof graph, and system of record — coordinated by four contract-scoped agents (construct, audit, prove, repair) and a two-stage orchestrator. By converting one brittle monolithic run into parallelized, CI-gated, locally recoverable transactions over a proof DAG, LeanMarathon successfully formalized all seven target theorems across four Erdős problems with zero sorry across three autonomous runs, proving 258 lemmas in total. The results argue that reliability in AI co-mathematics depends as much on durable system architecture as on prover strength.
formal-verificationautoformalizationtheorem-provingmulti-agent-systemsmathematical-reasoninglean-proverllm-reasoning
“LeanMarathon successfully formalizes all seven target theorems from two recent research papers spanning four Erdős problems with no sorry across three autonomous runs.”
paper / jasondeanlee / Jun 7
TAM (Torque Adaptation Module) is a learned, policy-agnostic module that corrects torque commands at runtime to compensate for dynamics mismatches — including sim-to-real gaps, unknown payloads, and inter-robot variability — without requiring real-robot data. It sits between the low-level controller and the robot's torque interface, using only proprioceptive history to compute residual torque corrections, making it reusable across policies with different action spaces (joint targets, end-effector targets, or direct torques). TAM is trained entirely in randomized simulation via multi-robot pretraining followed by robot-specific fine-tuning, offloading the need for domain randomization away from task policies. Zero-shot evaluation on a Franka Panda outperforms online system identification and RMA baselines across RL, BC, and MPC-based dynamic manipulation tasks.
roboticsrobot-learningmotion-transfersim-to-realmanipulationtorque-controldomain-randomization
“TAM can be reused across policies with different action spaces (joint targets, end-effector targets, direct torques) without retraining, because it depends only on proprioceptive history and not on policy observations or action space.”
paper / jasondeanlee / May 30
This paper addresses a gap in ICL theory: most prior work assumes all task-relevant information lives in the prompt, but practical ICL often requires retrieving facts stored in model weights. The authors formalize this as the "in-context factual recall" (IC-recall) task and prove that supervised fine-tuning of a one-layer transformer converges to a specific pairwise attention pattern that enables simultaneous relation inference from context and fact retrieval from an MLP associative memory. Crucially, this fine-tuning is sample-efficient, requiring only polylogarithmically many examples relative to the number of stored knowledge triplets.
in-context-learningtransformer-theoryfine-tuningfactual-recallllm-mechanistic-interpretabilityattention-mechanismsmachine-learning-theory
“Supervised fine-tuning of a one-layer transformer on IC-recall data converges to a specific pairwise attention pattern that enables in-context factual recall.”
paper / jasondeanlee / May 12 / failed
paper / jasondeanlee / May 12 / failed
paper / jasondeanlee / May 12 / failed