{"id":"arxiv/2602.16554","url":"https://arxiv.org/abs/2602.16554","tags":["cs.LO","cs.AI","cs.ET","quant-ph"],"score":0,"title":"MerLean: An Agentic Framework for Autoformalization in Quantum Computation","domain":"cs.LO","source":"arxiv","authors":["Yuanjie Ren","Jinzheng Li","Yidi Qi"],"reviews":0,"subject":"cs.LO","summary":"We introduce MerLean, a fully automated agentic framework for autoformalization in quantum computation. MerLean extracts mathematical statements from \\LaTeX{} source files, formalizes them into verified Lean~4 code built on Mathlib, and translates the result back into human-readable \\LaTeX{} for semantic review. We evaluate MerLean on three theoretical quantum computing papers producing 2,050 Lean declarations from 114 statements in total. MerLean achieves end-to-end formalization on all three papers, reducing the verification burden to only the newly introduced definitions and axioms. Our…","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"discussed":0,"published":"2026-02-18","reactions":{}}