Writing
Notes, announcements, and longer pieces — shared first on LinkedIn, kept here for the record.
-
Selected for the Google Antigravity science program
The Google Antigravity science program gives up to 10,000 researchers six months of access to Gemini 4 Argon. I will use it in three ongoing collaborations, from ML4CO for underwater sensor networks to channel...
- AI-Assisted Research
- Underwater Networks
- Quantum Networks
- Molecular Communication
-
IEEE TWC, ICLR and arXiv now all cap submission volume
IEEE TWC accepts at most 36 new manuscripts per author per year, ICLR 2027 limits authors to 20 submissions, and arXiv now allows each submitter two submissions a month. The caps count papers, not...
- Academic Publishing
- Peer Review
- Research Integrity
- arXiv
-
OpenAI's 722 mathematics manuscripts: citations, withdrawals, and proof dependencies
One day after OpenAI released 722 AI-produced mathematics manuscripts, three were withdrawn. The withdrawals show why a release of this size needs a record of which results each proof relies on.
- Mathematics
- AI-Assisted Research
- Research Integrity
- Formal Verification
- Scholarly Publishing
-
Andrej Karpathy on LLMs and ASD-STE100 controlled English
ASD-STE100 prioritizes unambiguous wording. For research explanations, one claim per sentence may also make individual claims easier to check.
- ASD-STE100
- Large Language Models
- Scientific Writing
- Verification
-
ICLR 2027 registrations and the peer-review workload
The post examines the reported scale of ICLR 2027 abstract registrations and proposals for managing peer review, alongside concerns about their trade-offs.
- ICLR
- Peer Review
- Machine Learning
- Research Assessment
-
Relevance ranking in RAG-based literature review: Jev versus embedding-based classifiers in quantum networking
A visual report compares Jev with Gemini Embedding 2 baselines on 594 quantum-networking papers, using full-text review to identify papers with explicit optimization formulations.
- RAG
- Literature Review
- Quantum Networking
- Information Retrieval
-
arXivisual: interactive visual explanations for research papers
arXivisual explores how research papers might be presented as interactive, scroll-driven visual explanations while retaining the paper as the rigorous reference record.
- Academic Publishing
- arXiv
- Open Source
- Scientific Visualization
-
What a Lean-verified forced Euler blow-up does — and does not — show
A remarkable development in AI-assisted analysis: finite-time singularity constructions for several forced fluid equations, paired with machine-checked formalizations. The qualification matters: the results concern forced equations, not the Clay Navier–Stokes problem.
- Fluid Mechanics
- Mathematical Analysis
- Lean
- AI-Assisted Research
- Formal Verification
-
Fermat's Last Theorem, formalized and checked by Lean
This is not a new proof of Fermat's Last Theorem. It is a computer-checked formalization of an existing proof — and a striking demonstration of what AI-assisted formal verification can make auditable.
- Formal Mathematics
- Lean
- AI-Assisted Research
- Mathematical Verification
-
The Internet of Algae: modelling communication across four signaling channels
Algae communicate through chemicals, voltage, and light. Internet of Algae Lab brings four signaling modalities into parameter-driven browser simulations.
- Molecular Communication
- Computational Biology
- Scientific Visualization
- Open Science
-
A second brain for AI-assisted work does not require Obsidian
Files alone do not prevent hallucinations; the agent's map must require evidence, citations where possible, and an explicit ‘not found’ when evidence is absent.
- Second Brain
- AI Agents
- Agentic Coding
- Context Engineering
-
AI safety claims need controls across every access path
Safety claims should be supported by evidence that controls work on every access path and produce auditable records.
- AI Safety
- AI Governance
- Responsible AI
-
Tracing AI-assisted research with research-graph
A traceability check can show whether the recorded workflow meets its rules; it cannot establish that a scientific result is correct.
- Graph Engineering
- Research Integrity
- AI Agents
- Reproducible Research
- Open Source
-
The AI Layoff Trap
The model frames AI-driven layoffs as a coordination problem: each firm captures its own saving while sharing the resulting demand loss with competitors.
- Artificial Intelligence
- Automation
- Labour Economics
-
Where ChatGPT Pro reasoning fits in a research workflow
Longer reasoning is most valuable when a shallow answer is costly—but it should still be challenged before it becomes code or an experiment.
- AI Research
- Large Language Models
- Research Workflows
-
Would you fail a student based on a Claude watermark alone?
A watermark may indicate that text came into contact with Claude, but it cannot by itself distinguish generation from editing or establish authorship, intent, or cheating.
- Academic Integrity
- AI Watermarking
- Higher Education
-
Context management in long-running agentic coding sessions
Compaction removes accumulated context; delegation keeps task-specific reading out of the main window. Six practical guidelines separate those mechanisms and state what the observed telemetry can and cannot establish.
- Context Engineering
- Agentic Workflows
- LLM Engineering
-
An AI second brain can remember everything and still be wrong
Search can recover a relevant record without knowing whether it is current, authoritative, or supported. A reliable AI second brain needs connected records, checks, and human review.
- AI Agents
- Knowledge Management
- Reproducible Research
-
Can LLMs really not jump, or are we defining the jump incorrectly?
Co-Scientist and an AI-assisted graph-theory counterexample complicate the claim that LLMs cannot make abductive jumps, but neither settles how scientific novelty should be defined.
- AI for Science
- Scientific Discovery
- Philosophy of Science
-
A 30-year gap in derivative-free convex optimization, closed with AI assistance and verified in Lean 4
Phillip Kerger reports a near-quadratic oracle-complexity lower bound for derivative-free convex optimization — open since Protasov's 1996 upper bound — drafted in a single 2.5-hour model session and formalized in Lean 4 with no...
- Optimization
- AI for Mathematics
- Formal Verification
-
Visually convincing LLM simulations can conceal substantial differences in numerical fidelity
Five frontier models built the same 3D underwater-acoustic solver in isolation. Judged against BELLHOP3D by numerical output rather than screenshots, visually convincing simulations concealed large gaps in fidelity.
- LLM Evaluation
- Underwater Acoustics
- Computational Physics
-
A university timetable can look clean on paper and still break in operation
KAIROS is a CP-SAT university timetabling engine that drove every hard-constraint category to zero across two live TED University terms — cutting within-day idle time ~75% and capacity waste ~29% per room-hour.
- Operations Research
- Constraint Programming
- University Timetabling
-
Still uploading your .tex files to Overleaf's servers?
I stopped a while ago. VS Code + LaTeX Workshop + Claude Code — files on disk, version control in Git, compilation on my own machine. Overleaf still wins on real-time collaboration; local control...
- LaTeX
- Scientific Writing
- Research Workflow
-
An academic rate limiter: IEEE TWC now caps authors at 36 new manuscripts a year
IEEE Transactions on Wireless Communications has introduced a per-author submission cap — at most 36 new manuscripts per year. Three a month. The number is high enough to be no constraint at all for...
- Academic Publishing
- Research Integrity
- Peer Review
-
The hardest part of running a jury isn't the jury
Three hours of evaluation can turn into days of Excel merging, score normalization, and accreditation paperwork. VERA turns post-jury work into a structured, export-ready workflow — QR-code scoring from a phone, live rankings, and...
- Engineering Education
- Assessment
- Accreditation
-
A 30,000-variable knapsack, solved on a GPU in ten seconds
NVIDIA cuOpt on a large-scale Multi-Dimensional Knapsack Problem — 30K binary variables, 10 knapsack constraints, ~300k nonzeros. Solved on a Tesla T4 under a 10-second limit to a ~0.035% relative MIP gap.
- Operations Research
- GPU Optimization
- Integer Programming
-
Airport gate assignment, revisited as a multi-objective mixed-integer program
A mixed-integer formulation of the airport gate assignment problem: time-overlap constraints via slot discretization, passenger-based gate capacities derived from historic utilization, and an objective that trades remote-stand penalties against passenger load balance.
- Operations Research
- Multi-Objective Optimization
- Integer Programming