@misc{arxiv-2604.00554v1.r13, title = {{A new mathematics retrieval system}}, year = {2010}, doi = {10.1145/1871437.1871635}, note = {Shahab Kamali and Frank Wm. Tompa. 2010. A new mathematics retrieval system. In Proc. ACM CIKM. 1413–1416. doi:10.1145/1871437.1871635}, } @misc{arxiv-2602.16554v1.r15, title = {{A Promising Path Towards Autoformalization and General Artificial Intelligence}}, year = {2020}, note = {Christian Szegedy (ed.). A Promising Path Towards Autoformalization and General Artificial Intelligence, 2020.}, } @misc{arxiv-2406.01940v2.r1, author = {Achiam, Josh and Adler, Steven and Agarwal, Sandhini and Ahmad, Lama and Akkaya, Ilge and Florencia Leoni Aleman and Almeida, Diogo and Altenschmidt, Janko and Altman, Sam and Anadkat, Shyamal}, title = {{Gpt-4 technical report}}, year = {2023}, url = {https://arxiv.org/abs/2303.08774}, note = {Josh Achiam, Steven Adler, Sandhini Agarwal, Lama Ahmad, Ilge Akkaya, Florencia Leoni Aleman, Diogo Almeida, Janko Altenschmidt, Sam Altman, Shyamal Anadkat, et al. Gpt-4 technical report. arXiv preprint arXiv:2303.08774, 2023.}, } @misc{arxiv-2512.09874v3.r1, author = {Adhikari, N.S. and Agarwal, S.}, title = {{A comparative study of pdf parsing tools across diverse document categories}}, year = {2025}, note = {Adhikari, N.S., Agarwal, S.: A comparative study of pdf parsing tools across diverse document categories. arXiv preprint (2025)}, } @misc{arxiv-2512.09874v3.r2, author = {Aguilar, F.D. and Hirata, N.S.}, title = {{ExpressMatch: A system for creating ground-truthed datasets of online mathematical expressions}}, year = {2012}, note = {Aguilar, F.D., Hirata, N.S.: ExpressMatch: A system for creating ground-truthed datasets of online mathematical expressions. In: Proceedings of the 10th IAPR International Workshop on Document Analysis Systems (DAS). pp. 155–159 (2012)}, } @misc{arxiv-2406.01940v2.r26, author = {Albert Qiaochu Jiang and Welleck, Sean and Jin Peng Zhou and Lacroix, Timoth{\'{e}}e and Liu, Jiacheng and Li, Wenda and Jamnik, Mateja and Lample, Guillaume and Wu, Yuhuai}, title = {{Draft, sketch, and prove: Guiding formal theorem provers with informal proofs}}, year = {2023}, url = {https://openreview.net/pdf?id=SMa9EAovKMC}, note = {Albert Qiaochu Jiang, Sean Welleck, Jin Peng Zhou, Timoth{\'{e}}e Lacroix, Jiacheng Liu, Wenda Li, Mateja Jamnik, Guillaume Lample, and Yuhuai Wu. Draft, sketch, and prove: Guiding formal theorem provers with informal proofs. In The Eleventh International Conference on Learning Representations, ICLR 2023, Kigali, Rwanda, May 1-5, 2023. OpenReview.net, 2023c. URL https://openreview.net/pdf?id=SMa9EAovKMC.}, } @misc{arxiv-2512.09874v3.r3, author = {Alvaro, F. and S{\'{a}}nchez, J.A. and Benedi, J.M.}, title = {{Unbiased evaluation of handwritten mathematical expression recognition}}, year = {2012}, note = {Alvaro, F., S{\'{a}}nchez, J.A., Benedi, J.M.: Unbiased evaluation of handwritten math- ematical expression recognition. In: Proceedings of the International Conference on Frontiers in Handwriting Recognition (ICFHR). pp. 181–186 (2012)}, } @misc{arxiv-2003.08005v1.r11, author = {Alvaro, F. and Zanibbi, R.}, title = {{A shape-based layout descriptor for classifying spatial relationships in handwritten math}}, year = {2013}, note = {F. Alvaro and R. Zanibbi, “A shape-based layout descriptor for classifying spatial relationships in handwritten math,” in Proceedings of the 2013 ACM symposium on Document engineering. ACM, 2013, pp. 123–126.}, } @misc{arxiv-2406.01940v2.r2, author = {Anthropic}, title = {{Introducing the next generation of claude}}, year = {2024}, url = {https://www.anthropic.com/news/claude-3-family}, note = {Anthropic. Introducing the next generation of claude, 2024. URL https://www.anthropic. com/news/claude-3-family.}, } @misc{arxiv-2601.22554v1.r1, title = {{Aristotle: IMO-Level Automated Theorem Proving}}, year = {2025}, doi = {10.48550/arXiv.2510.01346}, url = {https://doi.org/10.48550/arXiv.2510.01346}, note = {Tudor Achim, Alex Best, Alberto Bietti, Kevin Der, Mathïs F{\'{e}}d{\'{e}}rico, Sergei Gukov, Daniel Halpern- Leistner, Kirsten Henningsgard, Yury Kudryashov, Alexander Meiburg, et al. Aristotle: IMO-Level Automated Theorem Proving. arXiv preprint, 2025. doi: 10.48550/arXiv.2510.01346. URL https: //doi.org/10.48550/arXiv.2510.01346.}, } @misc{arxiv-2602.16554v1.r1, author = {arXiv}, title = {{arXiv quantum physics submission statistics}}, year = {2025}, url = {https://arxiv.org/year/quant-ph}, note = {arXiv. arXiv quantum physics submission statistics. https://arxiv.org/year/quant-ph, 2025.}, } @misc{arxiv-2406.01940v2.r29, year = {2024}, note = {Jia LI, Edward Beeching, Lewis Tunstall, Ben Lipkin, Roman Soletskyi, Shengyi Costa Huang, Kashif Rasul, Longhui Yu, Albert Jiang, Ziju Shen, Zihan Qin, Bin Dong, Li Zhou, Yann Fleureau, Guillaume Lample, and Stanislas Polu. Numinamath. [https://huggingface. co/AI-MO/NuminaMath-CoT](https://github.com/project-numina/ aimo-progress-prize/blob/main/report/numina_dataset.pdf), 2024.}, } @misc{arxiv-2512.09874v3.r10, year = {2025}, note = {Gemini Team, Google DeepMind: Gemini 2.5: Pushing the frontier with advanced reasoning, multimodality, long context, and next generation agentic capabilities. arXiv preprint (2025)}, } @misc{arxiv-2512.09874v3.r11, year = {2025}, url = {https://blog.google/products/gemini/gemini-3/}, note = {Google DeepMind: Gemini 3: Introducing the latest gemini ai model from google. https://blog.google/products/gemini/gemini-3/ (2025), accessed: 2025-12-01}, } @misc{arxiv-2512.09874v3.r18, year = {2024}, url = {https://www.llamaindex.ai/llamaparse}, note = {LlamaIndex: LlamaParse: Genai-native document parsing platform. https://www.llamaindex.ai/llamaparse (2024), accessed: 2025-12-01}, } @misc{arxiv-2512.09874v3.r21, year = {2025}, url = {https://mathpix.com}, note = {Mathpix, Inc.: Mathpix: Document conversion for stem. https://mathpix.com (2025), accessed: 2025-11-28}, } @misc{arxiv-2512.09874v3.r22, year = {2025}, url = {https://mistral.ai/news/mistral-ocr}, note = {Mistral AI: Mistral OCR 25.05: Next-generation document understanding model. https://mistral.ai/news/mistral-ocr (2025), accessed: 2025-11-28}, } @misc{arxiv-2512.09874v3.r23, year = {2025}, url = {https://huggingface.co/nanonets/Nanonets-OCR-s}, note = {Nano Net Technologies Inc.: Nanonets-OCR-s: Image-to-markdown ocr model. Hugging Face Model, https://huggingface.co/nanonets/Nanonets-OCR-s (2025), accessed: 2025-11-28}, } @misc{arxiv-2512.09874v3.r24, year = {2025}, url = {https://huggingface.co/datasets/getomni-ai/ocr-benchmark}, note = {OmniAI Technology, Inc.: Omni OCR Benchmark. Hugging Face Dataset, https://huggingface.co/datasets/getomni-ai/ocr-benchmark (2025), ac- cessed: 2025-11-17}, } @misc{arxiv-2512.09874v3.r25, year = {2025}, url = {https://openai.com/index/introducing-gpt-5/}, note = {OpenAI: GPT-5: Openai’s next generation language model. https://openai.com/index/introducing-gpt-5/ (2025), accessed: 2025-12- 01}, } @misc{arxiv-2512.09874v3.r30, year = {2025}, url = {https://github.com/pymupdf/PyMuPDF4LLM}, note = {PyMuPDF Contributors: PyMuPDF4LLM: Pdf extraction for large language mod- els. GitHub repository, https://github.com/pymupdf/PyMuPDF4LLM (2025), ac- cessed: 2025-12-01}, } @misc{arxiv-2512.09874v3.r31, year = {2025}, url = {https://github.com/py-pdf/pypdf}, note = {pypdf Contributors: pypdf: A pure-python pdf library. GitHub repository, https://github.com/py-pdf/pypdf (2025), accessed: 2025-12-01}, } @misc{arxiv-2512.09874v3.r32, year = {2025}, note = {Qwen Team: Qwen3-vl technical report. arXiv preprint (2025)}, } @misc{arxiv-2512.09874v3.r33, year = {2025}, url = {https://github.com/rednote-hilab/dots.ocr}, note = {RedNote HiLab: dots.ocr: Multilingual document layout parsing. GitHub reposi- tory, https://github.com/rednote-hilab/dots.ocr (2025), accessed: 2025-11-28}, } @misc{arxiv-2602.16554v1.r13, year = {1994}, doi = {10.1007/BFb0030541}, url = {http://link.springer.com/10.1007/BFb0030541}, note = {Lawrence C. Paulson (ed.). Isabelle, volume 828 of Lecture Notes in Computer Science. Springer- Verlag, Berlin/Heidelberg, 1994. ISBN 978-3-540-58244-1. doi: 10.1007/BFb0030541. URL http://link.springer.com/10.1007/BFb0030541.}, } @article{arxiv-2003.08005v1.r21, title = {{Automatic extraction of printed mathematical formulas using fuzzy logic and propagation of context}}, year = {2001}, note = {A. Kacem, A. Bela¨{\i}d, and M. B. Ahmed, “Automatic extraction of printed mathematical formulas using fuzzy logic and propagation of context,” International Journal on Document Analysis and Recognition, vol. 4, no. 2, pp. 97–108, 2001.}, } @misc{arxiv-2512.09874v3.r4, author = {Awal, A.M.A.M. and Mouch{\`{e}}re, H. and Viard-Gaudin, C.}, title = {{Towards handwritten mathematical expressions recognition}}, year = {2009}, note = {Awal, A.M.A.M., Mouch{\`{e}}re, H., Viard-Gaudin, C.: Towards handwritten mathe- matical expressions recognition. In: Proceedings of the 10th International Confer- ence on Document Analysis and Recognition (ICDAR). pp. 1046–1050 (2009)}, } @misc{arxiv-2406.01940v2.r4, author = {Azerbayev, Zhangir and Schoelkopf, Hailey and Paster, Keiran and Marco Dos Santos and McAleer, Stephen and Jiang, Albert Q. and Deng, Jia and Biderman, Stella and Welleck, Sean}, title = {{Llemma: An open language model for mathematics}}, year = {2023}, doi = {10.48550/arXiv.2310.10631}, url = {https://doi.org/10.48550/arXiv.2310.10631}, note = {Zhangir Azerbayev, Hailey Schoelkopf, Keiran Paster, Marco Dos Santos, Stephen McAleer, Albert Q. Jiang, Jia Deng, Stella Biderman, and Sean Welleck. Llemma: An open language model for mathematics. CoRR, abs/2310.10631, 2023b. doi: 10.48550/ARXIV.2310.10631. URL https: //doi.org/10.48550/arXiv.2310.10631.}, } @misc{arxiv-2406.01940v2.r3, author = {Azerbayev, Zhangir and Piotrowski, Bartosz and Schoelkopf, Hailey and Ayers, Edward W. and Radev, Dragomir and Avigad, Jeremy}, title = {{Proofnet: Autoformalizing and formally proving undergraduate-level mathematics}}, year = {2023}, doi = {10.48550/arXiv.2302.12433}, url = {https://doi.org/10.48550/arXiv.2302.12433}, note = {Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W. Ayers, Dragomir Radev, and Jeremy Avigad. Proofnet: Autoformalizing and formally proving undergraduate-level mathematics. CoRR, abs/2302.12433, 2023a. doi: 10.48550/ARXIV.2302.12433. URL https://doi.org/ 10.48550/arXiv.2302.12433.}, } @misc{arxiv-2406.01940v2.r5, author = {Bai, Yuntao and Kadavath, Saurav and Kundu, Sandipan and Askell, Amanda and Kernion, Jackson and Jones, Andy and Chen, Anna and Goldie, Anna and Mirhoseini, Azalia and McKinnon, Cameron and Chen, Carol and Olsson, Catherine and Olah, Christopher and Hernandez, Danny and Drain, Dawn and Ganguli, Deep and Li, Dustin and Tran-Johnson, Eli and Perez, Ethan and Kerr, Jamie and Mueller, Jared and Ladish, Jeffrey and Landau, Joshua and Ndousse, Kamal and Lukosiute, Kamile and Lovitt, Liane and Sellitto, Michael and Elhage, Nelson and Schiefer, Nicholas and Mercado, Noemí and DasSarma, Nova and Lasenby, Robert and Larson, Robin and Ringer, Sam and Johnston, Scott and Kravec, Shauna and Sheer El Showk and Fort, Stanislav and Lanham, Tamera and Telleen-Lawton, Timothy and Conerly, Tom and Henighan, Tom and Hume, Tristan and Bowman, Samuel R. and Hatfield-Dodds, Zac and Mann, Ben and Amodei, Dario and Joseph, Nicholas and McCandlish, Sam and Brown, Tom and Kaplan, Jared}, title = {{Constitutional AI: harmlessness from AI feedback}}, year = {2022}, doi = {10.48550/arXiv.2212.08073}, url = {https://doi.org/10.48550/arXiv.2212.08073}, note = {Yuntao Bai, Saurav Kadavath, Sandipan Kundu, Amanda Askell, Jackson Kernion, Andy Jones, Anna Chen, Anna Goldie, Azalia Mirhoseini, Cameron McKinnon, Carol Chen, Catherine Olsson, Christopher Olah, Danny Hernandez, Dawn Drain, Deep Ganguli, Dustin Li, Eli Tran-Johnson, Ethan Perez, Jamie Kerr, Jared Mueller, Jeffrey Ladish, Joshua Landau, Kamal Ndousse, Kamile Lukosiute, Liane Lovitt, Michael Sellitto, Nelson Elhage, Nicholas Schiefer, Noemí Mercado, Nova DasSarma, Robert Lasenby, Robin Larson, Sam Ringer, Scott Johnston, Shauna Kravec, Sheer El Showk, Stanislav Fort, Tamera Lanham, Timothy Telleen-Lawton, Tom Conerly, Tom Henighan, Tristan Hume, Samuel R. Bowman, Zac Hatfield-Dodds, Ben Mann, Dario Amodei, Nicholas Joseph, Sam McCandlish, Tom Brown, and Jared Kaplan. Constitutional AI: harmlessness from AI feedback. CoRR, abs/2212.08073, 2022. doi: 10.48550/ARXIV.2212.08073. URL https://doi.org/10.48550/arXiv.2212.08073.}, } @misc{arxiv-2406.01940v2.r6, author = {Barras, Bruno and Boutin, Samuel and Cornes, Cristina and Courant, Judica{\"e}l and Filli{\^{a}}tre, Jean-Christophe and Gim{\'{e}}nez, Eduardo and Herbelin, Hugo and Huet, G{\'{e}}rard P. and Muñoz, C{\'{e}}sar A. and Murthy, Chetan R. and Parent, Catherine and Paulin-Mohring, Christine and Saïbi, Amokrane and Werner, Benjamin}, title = {{The coq proof assistant : reference manual, version 6.1}}, year = {1997}, url = {https://api.semanticscholar.org/CorpusID:54117279}, note = {Bruno Barras, Samuel Boutin, Cristina Cornes, Judica{\"e}l Courant, Jean-Christophe Filli{\^{a}}tre, Eduardo Gim{\'{e}}nez, Hugo Herbelin, G{\'{e}}rard P. Huet, C{\'{e}}sar A. Muñoz, Chetan R. Murthy, Catherine Parent, Christine Paulin-Mohring, Amokrane Saïbi, and Benjamin Werner. The coq proof assistant : reference manual, version 6.1. 1997. URL https://api.semanticscholar.org/ CorpusID:54117279.}, } @misc{arxiv-2604.00554v1.r1, author = {Barrow, J. and Jain, R. and Morariu, V. and Manjunatha, V. and Oard, D.W. and Resnik, P.}, title = {{A joint model for document segmentation and segment labeling}}, year = {2020}, note = {J. Barrow, R. Jain, V. Morariu, V. Manjunatha, D.W. Oard, and P. Resnik. 2020. A joint model for document segmentation and segment labeling. In Proceedings of the 58th Annual Meeting of the Association for Computational Linguistics. 313–322.}, } @misc{arxiv-2512.09874v3.r5, author = {Bast, H. and Korzen, C.}, title = {{A benchmark and evaluation for text extraction from pdf}}, year = {2017}, note = {Bast, H., Korzen, C.: A benchmark and evaluation for text extraction from pdf. In: Proceedings of the ACM/IEEE Joint Conference on Digital Libraries (JCDL). pp. 1–10 (2017)}, } @misc{arxiv-2406.01940v2.r7, author = {Bauer, Andrej and Petkovic, Matej and Todorovski, Ljupco}, title = {{MLFMF: data sets for machine learning for mathematical formalization}}, year = {2023}, url = {http://papers.nips.cc/paper_files/paper/2023/hash/9efe8db7fab57e19eed25718abedbbd2-Abstract-Datasets_and_Benchmarks.html}, note = {Andrej Bauer, Matej Petkovic, and Ljupco Todorovski. MLFMF: data sets for machine learning for mathematical formalization. In Alice Oh, Tristan Naumann, Amir Globerson, Kate Saenko, Moritz Hardt, and Sergey Levine (eds.), Advances in Neural Information Processing Systems 36: Annual Conference on Neural Information Processing Systems 2023, NeurIPS 2023, New Orleans, LA, USA, December 10 - 16, 2023, 2023. URL http://papers.nips.cc/paper_files/paper/ 2023/hash/9efe8db7fab57e19eed25718abedbbd2-Abstract-Datasets_ and_Benchmarks.html.}, } @article{arxiv-2604.00554v1.r2, author = {Beck, Marco and Beckenbach, Isabel and Hartmann, Thomas and Schubotz, Moritz and Teschke, Olaf}, title = {{Transforming Scanned zbMATH Volumes to LaTeX: Planning the Next Level Digitisation}}, year = {2020}, note = {Marco Beck, Isabel Beckenbach, Thomas Hartmann, Moritz Schubotz, and Olaf Teschke. 2020. Transforming Scanned zbMATH Volumes to LaTeX: Planning the Next Level Digitisation. European Mathematical Society Magazine 117 (2020), 49–52.}, } @misc{arxiv-2601.22554v1.r2, author = {Becker, Lars and de Frutos-Fern{\'{a}}ndez, María In{\'{e}}s and Diedering, Leo and van Doorn, Floris and Gou{\"e}zel, S{\'{e}}bastien and Jamneshan, Asgar and Karunus, Evgenia and van de Meent, Edward and Monticone, Pietro and Mulder-Sohn, Jasper}, title = {{A Blueprint for the Formalization of Carleson’s Theorem on Convergence of Fourier Series}}, year = {2025}, doi = {10.48550/arXiv.2405.06423}, url = {https://doi.org/10.48550/arXiv.2405.06423}, note = {Lars Becker, María In{\'{e}}s de Frutos-Fern{\'{a}}ndez, Leo Diedering, Floris van Doorn, S{\'{e}}bastien Gou{\"e}zel, Asgar Jamneshan, Evgenia Karunus, Edward van de Meent, Pietro Monticone, Jasper Mulder-Sohn, et al. A Blueprint for the Formalization of Carleson’s Theorem on Convergence of Fourier Series. arXiv preprint, 2025. doi: 10.48550/arXiv.2405.06423. URL https://doi.org/10.48550/arXiv.2405.06423.}, } @misc{arxiv-2604.00554v1.r3, author = {Blecher, L. and Cucurull, G. and Scialom, T. and Stojnic, R.}, title = {{Nougat: Neural optical understanding for academic documents}}, year = {2023}, url = {https://arxiv.org/abs/2308.13418}, note = {L. Blecher, G. Cucurull, T. Scialom, and R. Stojnic. 2023. Nougat: Neural optical understanding for academic documents. arXiv preprint (2023). arXiv:2308.13418}, } @misc{arxiv-2601.22554v1.r3, author = {Bolan, Matthew and Breitner, Joachim and Brox, Jose and Carlini, Nicholas and Carneiro, Mario and van Doorn, Floris and Dvorak, Martin and Goens, Andr{\'{e}}s and Hill, Aaron and Husum, Harald and Hern{\'{a}}n Ibarra Mejia and Kocsis, Zoltan A. and Bruno Le Floch and Amir Livne Bar-on and Luccioli, Lorenzo and McNeil, Douglas and Meiburg, Alex and Monticone, Pietro and Nielsen, Pace P. and Emmanuel Osalotioman Osazuwa and Paolini, Giovanni and Petracci, Marco and Reinke, Bernhard and Renshaw, David and Rossel, Marcus and Roux, Cody and Scanvic, J{\'{e}}r{\'{e}}my and Srinivas, Shreyas and Anand Rao Tadipatri and Tao, Terence and Tsyrklevich, Vlad and Vaquerizo-Villar, Fernando and Weber, Daniel and Zheng, Fan}, title = {{The Equational Theories Project: Advancing Collaborative Mathematical Research at Scale}}, year = {2025}, doi = {10.48550/arXiv.2512.07087}, url = {https://doi.org/10.48550/arXiv.2512.07087}, note = {Matthew Bolan, Joachim Breitner, Jose Brox, Nicholas Carlini, Mario Carneiro, Floris van Doorn, Martin Dvorak, Andr{\'{e}}s Goens, Aaron Hill, Harald Husum, Hern{\'{a}}n Ibarra Mejia, Zoltan A. Kocsis, Bruno Le Floch, Amir Livne Bar-on, Lorenzo Luccioli, Douglas McNeil, Alex Meiburg, Pietro Monticone, Pace P. Nielsen, Emmanuel Osalotioman Osazuwa, Giovanni Paolini, Marco Petracci, Bernhard Reinke, David Renshaw, Marcus Rossel, Cody Roux, J{\'{e}}r{\'{e}}my Scanvic, Shreyas Srinivas, Anand Rao Tadipatri, Terence Tao, Vlad Tsyrklevich, Fernando Vaquerizo-Villar, Daniel Weber, and Fan Zheng. The Equational Theories Project: Advancing Collaborative Mathematical Research at Scale. arXiv preprint, 2025. doi: 10.48550/arXiv.2512.07087. URL https://doi.org/10.48550/arXiv.2512.07087.}, } @misc{arxiv-2602.16554v1.r2, author = {Breen, Benjamin and Marco Del Tredici and McCarran, Jacob and Javier Aspuru Mijares and Weichen Winston Yin and Sulimany, Kfir and Taylor, Jacob M. and Koppens, Frank H. L. and Englund, Dirk}, title = {{Ax-Prover: A Deep Reasoning Agentic Framework for Theorem Proving in Mathematics and Quantum Physics}}, year = {2025}, url = {http://arxiv.org/abs/2510.12787}, note = {Benjamin Breen, Marco Del Tredici, Jacob McCarran, Javier Aspuru Mijares, Weichen Winston Yin, Kfir Sulimany, Jacob M. Taylor, Frank H. L. Koppens, and Dirk Englund. Ax-Prover: A Deep Reasoning Agentic Framework for Theorem Proving in Mathematics and Quantum Physics, November 2025. URL http://arxiv.org/abs/2510.12787. arXiv:2510.12787 [cs].}, } @article{arxiv-2602.16554v1.r3, author = {Breuckmann, Nikolas P and Jens Niklas Eberhardt}, title = {{Balanced product quantum codes}}, year = {2021}, note = {Nikolas P Breuckmann and Jens Niklas Eberhardt. Balanced product quantum codes. IEEE Transac- tions on Information Theory, 67(10):6653–6674, 2021.}, } @misc{arxiv-2604.00554v1.r4, author = {Brown, Tom and Mann, Benjamin and Ryder, Nick and Subbiah, Melanie and Kaplan, Jared D and Dhariwal, Prafulla and Neelakantan, Arvind and Shyam, Pranav and Sastry, Girish and Askell, Amanda}, title = {{Language models are few-shot learners}}, year = {2020}, note = {Tom Brown, Benjamin Mann, Nick Ryder, Melanie Subbiah, Jared D Kaplan, Prafulla Dhariwal, Arvind Neelakantan, Pranav Shyam, Girish Sastry, Amanda Askell, et al. 2020. Language models are few-shot learners. Advances in neural information processing systems 33 (2020), 1877–1901.}, } @misc{arxiv-2601.22554v1.r4, author = {Buzzard, Kevin and Taylor, Richard}, title = {{FLT: An Ongoing Lean Formalisation of the Proof of Fermat’s Last Theorem}}, year = {2023}, url = {https://github.com/ImperialCollegeLondon/FLT}, note = {Kevin Buzzard and Richard Taylor. FLT: An Ongoing Lean Formalisation of the Proof of Fermat’s Last Theorem, 2023. URL https://github.com/ImperialCollegeLondon/FLT.}, } @misc{arxiv-2604.00554v1.r5, author = {Cai, Zhaowei and Vasconcelos, Nuno}, title = {{Cascade r-cnn: Delving into high quality object detection}}, year = {2018}, note = {Zhaowei Cai and Nuno Vasconcelos. 2018. Cascade r-cnn: Delving into high quality object detection. In Proceedings of the IEEE conference on computer vision and pattern recognition. 6154–6162.}, } @misc{arxiv-2512.09874v3.r6, author = {Chao, H. and Fan, J.}, title = {{Layout and content extraction for PDF documents}}, year = {2004}, note = {Chao, H., Fan, J.: Layout and content extraction for PDF documents. In: Proceed- ings of the 6th International Workshop on Document Analysis Systems (DAS). pp. 213–224 (2004)}, } @misc{arxiv-2003.08005v1.r19, author = {Chaudhuri, B. and Garain, U.}, title = {{An approach for processing mathematical expressions in printed document}}, year = {1998}, note = {B. Chaudhuri and U. Garain, “An approach for processing mathematical expressions in printed document,” in International Workshop on Document Analysis Systems. Springer, 1998, pp. 310–321.}, } @misc{arxiv-2601.22554v1.r5, author = {Chen, Jiangjie and Chen, Wenxiang and Du, Jiacheng and Hu, Jinyi and Jiang, Zhicheng and Jie, Allan and Jin, Xiaoran and Jin, Xing and Li, Chenggang and Shi, Wenlei}, title = {{Seed-Prover 1.5: Mastering Undergraduate-Level Theorem Proving via Learning from Experience}}, year = {2025}, doi = {10.48550/arXiv.2512.17260}, url = {https://doi.org/10.48550/arXiv.2512.17260}, note = {Jiangjie Chen, Wenxiang Chen, Jiacheng Du, Jinyi Hu, Zhicheng Jiang, Allan Jie, Xiaoran Jin, Xing Jin, Chenggang Li, Wenlei Shi, et al. Seed-Prover 1.5: Mastering Undergraduate-Level Theorem Proving via Learning from Experience. arXiv preprint, 2025. doi: 10.48550/arXiv.2512.17260. URL https://doi.org/10.48550/arXiv.2512.17260.}, } @misc{arxiv-2406.01940v2.r8, author = {Chen, Jiaqi and Li, Tong and Qin, Jinghui and Lu, Pan and Lin, Liang and Chen, Chongyu and Liang, Xiaodan}, title = {{Unigeo: Unifying geometry logical reasoning via reformulating mathematical expression}}, year = {2022}, doi = {10.18653/v1/2022.emnlp-main.218}, url = {https://doi.org/10.18653/v1/2022.emnlp-main.218}, note = {Jiaqi Chen, Tong Li, Jinghui Qin, Pan Lu, Liang Lin, Chongyu Chen, and Xiaodan Liang. Unigeo: Unifying geometry logical reasoning via reformulating mathematical expression. In Yoav Goldberg, Zornitsa Kozareva, and Yue Zhang (eds.), Proceedings of the 2022 Conference on Empirical Methods in Natural Language Processing, EMNLP 2022, Abu Dhabi, United Arab Emirates, 11 December 7-11, 2022, pp. 3313–3323. Association for Computational Linguistics, 2022. doi: 10.18653/V1/2022.EMNLP-MAIN.218. URL https://doi.org/10.18653/v1/2022. emnlp-main.218.}, } @misc{arxiv-2601.22554v1.r6, author = {Chen, Luoxin and Gu, Jinming and Huang, Liankai and Huang, Wenhao and Jiang, Zhicheng and Jie, Allan and Jin, Xiaoran and Jin, Xing and Li, Chenggang and Ma, Kaijing}, title = {{Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving}}, year = {2025}, doi = {10.48550/arXiv.2507.23726}, url = {https://arxiv.org/abs/2507.23726}, note = {Luoxin Chen, Jinming Gu, Liankai Huang, Wenhao Huang, Zhicheng Jiang, Allan Jie, Xiaoran Jin, Xing Jin, Chenggang Li, Kaijing Ma, et al. Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving. arXiv preprint, 2025. doi: 10.48550/arXiv.2507.23726. URL https://doi.org/10.48550/arX iv.2507.23726.}, } @misc{arxiv-2406.01940v2.r9, author = {Chen, Mark and Tworek, Jerry and Jun, Heewoo and Yuan, Qiming and Henrique Pond{\'{e}} de Oliveira Pinto and Kaplan, Jared and Edwards, Harrison and Burda, Yuri and Joseph, Nicholas and Brockman, Greg and Ray, Alex and Puri, Raul and Krueger, Gretchen and Petrov, Michael and Khlaaf, Heidy and Sastry, Girish and Mishkin, Pamela and Chan, Brooke and Gray, Scott and Ryder, Nick and Pavlov, Mikhail and Power, Alethea and Kaiser, Lukasz and Bavarian, Mohammad and Winter, Clemens and Tillet, Philippe and Felipe Petroski Such and Cummings, Dave and Plappert, Matthias and Chantzis, Fotios and Barnes, Elizabeth and Herbert-Voss, Ariel and William Hebgen Guss and Nichol, Alex and Paino, Alex and Tezak, Nikolas and Tang, Jie and Babuschkin, Igor and Balaji, Suchir and Jain, Shantanu and Saunders, William and Hesse, Christopher and Carr, Andrew N. and Leike, Jan and Achiam, Joshua and Misra, Vedant and Morikawa, Evan and Radford, Alec and Knight, Matthew and Brundage, Miles and Murati, Mira and Mayer, Katie and Welinder, Peter and McGrew, Bob and Amodei, Dario and McCandlish, Sam and Sutskever, Ilya and Zaremba, Wojciech}, title = {{Evaluating large language models trained on code}}, year = {2021}, url = {https://arxiv.org/abs/2107.03374}, note = {Mark Chen, Jerry Tworek, Heewoo Jun, Qiming Yuan, Henrique Pond{\'{e}} de Oliveira Pinto, Jared Kaplan, Harrison Edwards, Yuri Burda, Nicholas Joseph, Greg Brockman, Alex Ray, Raul Puri, Gretchen Krueger, Michael Petrov, Heidy Khlaaf, Girish Sastry, Pamela Mishkin, Brooke Chan, Scott Gray, Nick Ryder, Mikhail Pavlov, Alethea Power, Lukasz Kaiser, Mohammad Bavarian, Clemens Winter, Philippe Tillet, Felipe Petroski Such, Dave Cummings, Matthias Plappert, Fotios Chantzis, Elizabeth Barnes, Ariel Herbert-Voss, William Hebgen Guss, Alex Nichol, Alex Paino, Nikolas Tezak, Jie Tang, Igor Babuschkin, Suchir Balaji, Shantanu Jain, William Saunders, Christopher Hesse, Andrew N. Carr, Jan Leike, Joshua Achiam, Vedant Misra, Evan Morikawa, Alec Radford, Matthew Knight, Miles Brundage, Mira Murati, Katie Mayer, Peter Welinder, Bob McGrew, Dario Amodei, Sam McCandlish, Ilya Sutskever, and Wojciech Zaremba. Evaluating large language models trained on code. CoRR, abs/2107.03374, 2021. URL https://arxiv. org/abs/2107.03374.}, } @misc{arxiv-2406.01940v2.r51, author = {Christian Szegedy}, title = {{A promising path towards autoformalization and general artificial intelligence}}, year = {2020}, doi = {10.1007/978-3-030-53518-6_1}, url = {https://doi.org/10.1007/978-3-030-53518-6_1}, note = {Christian Szegedy. A promising path towards autoformalization and general artificial intelligence. In Christoph Benzm{\"u}ller and Bruce R. Miller (eds.), Intelligent Computer Mathematics - 13th Interna- tional Conference, CICM 2020, Bertinoro, Italy, July 26-31, 2020, Proceedings, volume 12236 of Lecture Notes in Computer Science, pp. 3–20. Springer, 2020. doi: 10.1007/978-3-030-53518-6\_1. URL https://doi.org/10.1007/978-3-030-53518-6_1.}, } @misc{arxiv-2003.08005v1.r2, author = {Clark, C. and Divvala, S.}, title = {{Pdffigures 2.0: Mining figures from research papers}}, year = {2016}, note = {C. Clark and S. Divvala, “Pdffigures 2.0: Mining figures from research papers,” in 2016 IEEE/ACM Joint Conference on Digital Libraries (JCDL). IEEE, 2016, pp. 143–152.}, } @misc{arxiv-2604.00554v1.r6, author = {Clement, C.B. and Bierbaum, M. and O’Keeffe, K.P. and Alemi, A.A.}, title = {{On the use of arxiv as a dataset}}, year = {2019}, url = {https://arxiv.org/abs/1905.00075}, note = {C.B. Clement, M. Bierbaum, K.P. O’Keeffe, and A.A. Alemi. 2019. On the use of arxiv as a dataset. arXiv preprint (2019). arXiv:1905.00075}, } @misc{arxiv-2406.01940v2.r10, author = {Cobbe, Karl and Kosaraju, Vineet and Bavarian, Mohammad and Chen, Mark and Jun, Heewoo and Kaiser, Lukasz and Plappert, Matthias and Tworek, Jerry and Hilton, Jacob and Nakano, Reiichiro and Hesse, Christopher and Schulman, John}, title = {{Training verifiers to solve math word problems}}, year = {2021}, url = {https://arxiv.org/abs/2110.14168}, note = {Karl Cobbe, Vineet Kosaraju, Mohammad Bavarian, Mark Chen, Heewoo Jun, Lukasz Kaiser, Matthias Plappert, Jerry Tworek, Jacob Hilton, Reiichiro Nakano, Christopher Hesse, and John Schulman. Training verifiers to solve math word problems. CoRR, abs/2110.14168, 2021. URL https://arxiv.org/abs/2110.14168.}, } @misc{arxiv-2003.08005v1.r8, author = {Condon, M.}, title = {{Applying hierarchical contextual parsing with visual density and geometric features to typeset formula recognition}}, year = {2017}, note = {M. Condon, “Applying hierarchical contextual parsing with visual density and geometric features to typeset formula recognition,” Master’s thesis, Rochester Institute of Technology, Rochester, NY, USA, 2017.}, } @misc{arxiv-2512.09874v3.r8, author = {Cui, C. and Sun, T. and Lin, M. and Gao, T. and Zhang, Y. and Liu, J. and Wang, X. and Zhang, Z. and Zhou, C. and Liu, H. and Zhang, Y. and Lv, W. and Huang, K. and Zhang, Y. and Zhang, J. and Zhang, J. and Liu, Y. and Yu, D. and Ma, Y.}, title = {{Paddleocr 3.0 technical report}}, year = {2025}, note = {Cui, C., Sun, T., Lin, M., Gao, T., Zhang, Y., Liu, J., Wang, X., Zhang, Z., Zhou, C., Liu, H., Zhang, Y., Lv, W., Huang, K., Zhang, Y., Zhang, J., Zhang, J., Liu, Y., Yu, D., Ma, Y.: Paddleocr 3.0 technical report. arXiv preprint (2025)}, } @misc{arxiv-2512.09874v3.r7, author = {Cui, C. and Sun, T. and Liang, S. and Gao, T. and Zhang, Z. and Liu, J. and Wang, X. and Zhou, C. and Liu, H. and Lin, M. and Zhang, Y. and Zhang, Y. and Zheng, H. and Zhang, J. and Zhang, J. and Liu, Y. and Yu, D. and Ma, Y.}, title = {{Paddleocr-vl: Boosting multilingual document parsing via a 0.9b ultra-compact vision-language model}}, year = {2025}, note = {Cui, C., Sun, T., Liang, S., Gao, T., Zhang, Z., Liu, J., Wang, X., Zhou, C., Liu, H., Lin, M., Zhang, Y., Zhang, Y., Zheng, H., Zhang, J., Zhang, J., Liu, Y., Yu, D., Ma, Y.: Paddleocr-vl: Boosting multilingual document parsing via a 0.9b ultra-compact vision-language model. arXiv preprint (2025)}, } @misc{arxiv-2003.08005v1.r1, author = {Davila, K. and Joshi, R. and Setlur, S. and Govindaraju, V. and Zanibbi, R.}, note = {K. Davila, R. Joshi, S. Setlur, V. Govindaraju, and R. Zanibbi, “Tangent- v: Math formula image search using line-of-sight graphs,” in ECIR, ser. LNCS, vol. 11437, pp. 681–695.}, } @misc{arxiv-2604.00554v1.r7, author = {Davila, Kenny and Zanibbi, Richard}, title = {{Layout and Semantics: Combining Representations for Mathematical Formula Search}}, year = {2017}, doi = {10.1145/3077136.3080748}, note = {Kenny Davila and Richard Zanibbi. 2017. Layout and Semantics: Combining Representations for Mathematical Formula Search. In Proc. ACM SIGIR. 1165– 1168. doi:10.1145/3077136.3080748}, } @misc{arxiv-2601.22554v1.r8, author = {de Moura, Leonardo and Kong, Soonho and Avigad, Jeremy and van Doorn, Floris and von Raumer, Jakob}, title = {{The Lean Theorem Prover (System Description)}}, year = {2015}, doi = {10.1007/978-3-319-21401-6_26}, url = {https://doi.org/10.1007/978-3-319-21401-6_26}, note = {Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. The Lean Theorem Prover (System Description). In Automated Deduction – CADE-25, volume 9195 of Lecture Notes in Computer Science, pages 378–388. Springer, 2015. doi: 10.1007/978-3-319-21401-6_26. URL https://doi.org/10.1007/978-3-319-21401-6_26.}, } @misc{arxiv-2406.01940v2.r12, author = {de Moura, Leonardo and Ullrich, Sebastian}, title = {{The lean 4 theorem prover and programming language}}, year = {2021}, doi = {10.1007/978-3-030-79876-5_37}, url = {https://doi.org/10.1007/978-3-030-79876-5_37}, note = {Leonardo de Moura and Sebastian Ullrich. The lean 4 theorem prover and programming language. In Andr{\'{e}} Platzer and Geoff Sutcliffe (eds.), Automated Deduction - CADE 28 - 28th International Conference on Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings, volume 12699 of Lecture Notes in Computer Science, pp. 625–635. Springer, 2021. doi: 10.1007/ 978-3-030-79876-5\_37. URL https://doi.org/10.1007/978-3-030-79876-5_ 37.}, } @misc{arxiv-2601.22554v1.r7, author = {de Moura, Leonardo and Ullrich, Sebastian}, title = {{The Lean 4 Theorem Prover and Programming Language}}, year = {2021}, doi = {10.1007/978-3-030-79876-5_37}, note = {Leonardo de Moura and Sebastian Ullrich. The Lean 4 Theorem Prover and Programming Language. In Automated Deduction – CADE 28, volume 12699 of Lecture Notes in Computer Science, pages 625–635. Springer, 2021. doi: 10.1007/978-3-030-79876-5_37. URL https://doi.org/10.1007/978-3-030-798 76-5_37.}, } @misc{arxiv-2602.16554v1.r11, author = {de Moura, Leonardo and Ullrich, Sebastian}, title = {{The Lean 4 Theorem Prover and Programming Language}}, year = {2021}, doi = {10.1007/978-3-030-79876-5_37}, url = {https://doi.org/10.1007/978-3-030-79876-5_37}, note = {Leonardo de Moura and Sebastian Ullrich. The Lean 4 Theorem Prover and Programming Language. In Automated Deduction – CADE 28: 28th International Conference on Automated Deduction, Virtual Event, July 12–15, 2021, Proceedings, pp. 625–635, Berlin, Heidelberg, July 2021. Springer- Verlag. ISBN 978-3-030-79875-8. doi: 10.1007/978-3-030-79876-5 37. URL https://doi. org/10.1007/978-3-030-79876-5_37.}, } @misc{arxiv-2406.01940v2.r13, author = {de Moura, Leonardo Mendonça and Kong, Soonho and Avigad, Jeremy and van Doorn, Floris and von Raumer, Jakob}, title = {{The lean theorem prover (system description)}}, year = {2015}, doi = {10.1007/978-3-319-21401-6_26}, url = {https://doi.org/10.1007/978-3-319-21401-6_26}, note = {Leonardo Mendonça de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. The lean theorem prover (system description). In Amy P. Felty and Aart Middeldorp (eds.), Automated Deduction - CADE-25 - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings, volume 9195 of Lecture Notes in Computer Science, pp. 378–388. Springer, 2015. doi: 10.1007/978-3-319-21401-6\_26. URL https: //doi.org/10.1007/978-3-319-21401-6_26.}, } @misc{arxiv-2601.22554v1.r9, author = {Degenne, R{\'{e}}my and Ledvinka, David and Marion, Etienne and Pfaffelhuber, Peter}, title = {{Formalization of Brownian Motion in Lean}}, year = {2025}, doi = {10.48550/arXiv.2511.20118}, url = {https://arxiv.org/abs/2511.20118}, note = {R{\'{e}}my Degenne, David Ledvinka, Etienne Marion, and Peter Pfaffelhuber. Formalization of Brownian Motion in Lean. arXiv preprint, 2025. doi: 10.48550/arXiv.2511.20118. URL https://doi.org/10.485 50/arXiv.2511.20118.}, } @misc{arxiv-2003.08005v1.r33, author = {Deng, J. and Dong, W. and Socher, R. and Li, L.-J. and Li, K. and Fei-Fei, L.}, title = {{Imagenet: A large-scale hierarchical image database}}, year = {2009}, note = {J. Deng, W. Dong, R. Socher, L.-J. Li, K. Li, and L. Fei-Fei, “Imagenet: A large-scale hierarchical image database,” in 2009 IEEE conference on computer vision and pattern recognition. IEEE, 2009, pp. 248–255.}, } @misc{arxiv-2003.08005v1.r9, author = {Deng, Y. and Kanervisto, A. and Ling, J. and Rush, A. M.}, year = {2016}, url = {https://arxiv.org/abs/1609.04938}, note = {Y. Deng, A. Kanervisto, J. Ling, and A. M. Rush, “Image- to-markup generation with coarse-to-fine attention,” arXiv preprint arXiv:1609.04938, 2016.}, } @misc{arxiv-2512.09874v3.r9, author = {Deng, Y. and Kanervisto, A. and Ling, J. and Rush, A.M.}, title = {{Image-to-markup generation with coarse-to-fine attention}}, year = {2017}, note = {Deng, Y., Kanervisto, A., Ling, J., Rush, A.M.: Image-to-markup generation with coarse-to-fine attention. In: Proceedings of the 34th International Conference on Machine Learning (ICML). vol. 70, pp. 980–989 (2017)}, } @misc{arxiv-2602.16554v1.r4, title = {{Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs}}, year = {2022}, url = {http://arxiv.org/abs/2210.12283}, note = {Albert Q. Jiang, Sean Welleck, Jin Peng Zhou, Wenda Li, Jiacheng Liu, Mateja Jamnik, Timoth´ee Lacroix, Yuhuai Wu, and Guillaume Lample. Draft, Sketch, and Prove: Guiding Formal Theo- rem Provers with Informal Proofs, November 2022. URL http://arxiv.org/abs/2210. 12283. arXiv:2210.12283 [cs].}, } @misc{arxiv-2003.08005v1.r17, author = {Drake, D. M. and Baird, H. S.}, title = {{Distinguishing mathematics notation from english text using computational geometry}}, year = {2005}, note = {D. M. Drake and H. S. Baird, “Distinguishing mathematics notation from english text using computational geometry,” in Eighth International Conference on Document Analysis and Recognition (ICDAR’05). IEEE, 2005, pp. 1270–1274.}, } @article{arxiv-2604.00554v1.r25, title = {{Enhancing optical character recognition on images with mixed text using semantic segmentation}}, year = {2022}, note = {S. Patil, V. Varadarajan, S. Mahadevkar, R. Athawade, L. Maheshwari, S. Kumb- hare, Y. Garg, D. Dharrao, P. Kamat, and K. Kotecha. 2022. Enhancing optical character recognition on images with mixed text using semantic segmentation. Journal of Sensor and Actuator Networks 11, 4 (2022), 63.}, } @misc{arxiv-2003.08005v1.r32, title = {{Focal loss for dense object detection}}, year = {2017}, note = {T.-Y. Lin, P. Goyal, R. Girshick, K. He, and P. Doll´ar, “Focal loss for dense object detection,” in Proceedings of the IEEE international conference on computer vision, 2017, pp. 2980–2988.}, } @misc{arxiv-2406.01940v2.r14, author = {Gadgil, Siddhartha and Anand Rao Tadipatri and Agrawal, Ayush and Narayanan, Ashvni and Goyal, Navin}, title = {{Towards automating formalisation of theorem statements using large language models}}, year = {2022}, note = {Siddhartha Gadgil, Anand Rao Tadipatri, Ayush Agrawal, Ashvni Narayanan, and Navin Goyal. Towards automating formalisation of theorem statements using large language models. In 36th Conference on Neural Information Processing Systems (NeurIPS 2022) Workshop on MATH-AI, 2022.}, } @misc{arxiv-2003.08005v1.r18, author = {Gao, L. and Yi, X. and Liao, Y. and Jiang, Z. and Yan, Z. and Tang, Z.}, title = {{A deep learning-based formula detection method for pdf documents}}, year = {2017}, note = {L. Gao, X. Yi, Y. Liao, Z. Jiang, Z. Yan, and Z. Tang, “A deep learning- based formula detection method for pdf documents,” in 2017 14th IAPR International Conference on Document Analysis and Recognition (ICDAR), vol. 1. IEEE, 2017, pp. 553–558.}, } @misc{arxiv-2406.01940v2.r15, author = {Gao, Luyu and Dai, Zhuyun and Pasupat, Panupong and Chen, Anthony and Arun Tejasvi Chaganty and Fan, Yicheng and Zhao, Vincent Y. and Lao, Ni and Lee, Hongrae and Juan, Da-Cheng and Guu, Kelvin}, title = {{RARR: researching and revising what language models say, using language models}}, year = {2023}, doi = {10.18653/v1/2023.acl-long.910}, url = {https://doi.org/10.18653/v1/2023.acl-long.910}, note = {Luyu Gao, Zhuyun Dai, Panupong Pasupat, Anthony Chen, Arun Tejasvi Chaganty, Yicheng Fan, Vincent Y. Zhao, Ni Lao, Hongrae Lee, Da-Cheng Juan, and Kelvin Guu. RARR: researching and revising what language models say, using language models. In Anna Rogers, Jordan L. Boyd- Graber, and Naoaki Okazaki (eds.), Proceedings of the 61st Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), ACL 2023, Toronto, Canada, July 9-14, 2023, pp. 16477–16508. Association for Computational Linguistics, 2023. doi: 10.18653/V1/2023. ACL-LONG.910. URL https://doi.org/10.18653/v1/2023.acl-long.910.}, } @misc{arxiv-2003.08005v1.r20, author = {Garain, U. and Chaudhuri, B.}, title = {{A syntactic approach for processing mathematical expressions in printed documents}}, year = {2000}, note = {U. Garain and B. Chaudhuri, “A syntactic approach for processing mathematical expressions in printed documents,” in Proceedings 15th International Conference on Pattern Recognition. ICPR-2000, vol. 4. IEEE, 2000, pp. 523–526.}, } @misc{arxiv-2003.08005v1.r14, author = {Garain, U. and Chaudhuri, B. B.}, title = {{Ocr of printed mathematical expressions}}, year = {2007}, note = {U. Garain and B. B. Chaudhuri, “Ocr of printed mathematical expressions,” in Digital Document Processing. Springer, 2007, pp. 235–259.}, } @misc{arxiv-2003.08005v1.r24, author = {Girshick, R. and Donahue, J. and Darrell, T. and Malik, J.}, title = {{Rich feature hierarchies for accurate object detection and semantic segmentation}}, year = {2014}, note = {R. Girshick, J. Donahue, T. Darrell, and J. Malik, “Rich feature hierarchies for accurate object detection and semantic segmentation,” in Proceedings of the IEEE conference on computer vision and pattern recognition, 2014, pp. 580–587.}, } @misc{arxiv-2003.08005v1.r25, author = {Girshick, R.}, title = {{Fast r-cnn}}, year = {2015}, note = {R. Girshick, “Fast r-cnn,” in Proceedings of the IEEE international conference on computer vision, 2015, pp. 1440–1448.}, } @misc{arxiv-2601.22554v1.r10, author = {Google DeepMind}, title = {{Formal Conjectures: A Collection of Formalized Statements of Conjectures in Lean}}, year = {2025}, url = {https://github.com/google-deepmind/formal-conjectures}, note = {Google DeepMind. Formal Conjectures: A Collection of Formalized Statements of Conjectures in Lean, 2025. URL https://github.com/google-deepmind/formal-conjectures.}, } @misc{arxiv-2406.01940v2.r16, author = {Gou, Zhibin and Shao, Zhihong and Gong, Yeyun and Shen, Yelong and Yang, Yujiu and Duan, Nan and Chen, Weizhu}, title = {{CRITIC: large language models can self-correct with tool-interactive critiquing}}, year = {2023}, doi = {10.48550/arXiv.2305.11738}, url = {https://doi.org/10.48550/arXiv.2305.11738}, note = {Zhibin Gou, Zhihong Shao, Yeyun Gong, Yelong Shen, Yujiu Yang, Nan Duan, and Weizhu Chen. CRITIC: large language models can self-correct with tool-interactive critiquing. CoRR, abs/2305.11738, 2023. doi: 10.48550/ARXIV.2305.11738. URL https://doi.org/10. 48550/arXiv.2305.11738.}, } @misc{arxiv-2604.00554v1.r8, author = {Greiner-Petter, Andr{\'{e}} and Schubotz, Moritz and M{\"u}ller, Fabian and Breitinger, Corinna and Cohl, Howard and Aizawa, Akiko and Gipp, Bela}, title = {{Discovering Mathematical Objects of Interest—A Study of Mathematical Notations}}, year = {2020}, doi = {10.1145/3366423.3380218}, note = {Andr{\'{e}} Greiner-Petter, Moritz Schubotz, Fabian M{\"u}ller, Corinna Breitinger, Howard Cohl, Akiko Aizawa, and Bela Gipp. 2020. Discovering Mathemati- cal Objects of Interest—A Study of Mathematical Notations. In Proceedings of The Web Conference 2020 (WWW ’20). Association for Computing Machinery, New York, NY, USA, 1445–1456. doi:10.1145/3366423.3380218}, } @misc{arxiv-2406.01940v2.r17, author = {Gunasekar, Suriya and Zhang, Yi and Aneja, Jyoti and Caio C{\'{e}}sar Teodoro Mendes and Allie Del Giorno and Gopi, Sivakanth and Javaheripi, Mojan and Kauffmann, Piero and de Rosa, Gustavo and Saarikivi, Olli and Salim, Adil and Shah, Shital and Harkirat Singh Behl and Wang, Xin and Bubeck, S{\'{e}}bastien and Eldan, Ronen and Adam Tauman Kalai and Yin Tat Lee and Li, Yuanzhi}, title = {{Textbooks are all you need}}, year = {2023}, doi = {10.48550/arXiv.2306.11644}, url = {https://doi.org/10.48550/arXiv.2306.11644}, note = {Suriya Gunasekar, Yi Zhang, Jyoti Aneja, Caio C{\'{e}}sar Teodoro Mendes, Allie Del Giorno, Sivakanth Gopi, Mojan Javaheripi, Piero Kauffmann, Gustavo de Rosa, Olli Saarikivi, Adil Salim, Shital Shah, Harkirat Singh Behl, Xin Wang, S{\'{e}}bastien Bubeck, Ronen Eldan, Adam Tauman Kalai, Yin Tat Lee, and Yuanzhi Li. Textbooks are all you need. CoRR, abs/2306.11644, 2023. doi: 10. 48550/ARXIV.2306.11644. URL https://doi.org/10.48550/arXiv.2306.11644.}, } @misc{arxiv-2604.00554v1.r9, author = {He, Kaiming and Gkioxari, Georgia and Doll{\'{a}}r, Piotr and Girshick, Ross}, title = {{Mask r-cnn}}, year = {2017}, note = {Kaiming He, Georgia Gkioxari, Piotr Doll{\'{a}}r, and Ross Girshick. 2017. Mask r-cnn. In Proceedings of the IEEE international conference on computer vision. 2961–2969.}, } @misc{arxiv-2406.01940v2.r20, author = {Hendrycks, Dan and Burns, Collin and Kadavath, Saurav and Arora, Akul and Basart, Steven and Tang, Eric and Song, Dawn and Steinhardt, Jacob}, title = {{Measuring mathematical problem solving with the MATH dataset}}, year = {2021}, url = {https://datasets-benchmarks-proceedings.neurips.cc/paper/2021/hash/be83ab3ecd0db773eb2dc1b0a17836a1-Abstract-round2.html}, note = {Dan Hendrycks, Collin Burns, Saurav Kadavath, Akul Arora, Steven Basart, Eric Tang, Dawn Song, and Jacob Steinhardt. Measuring mathematical problem solving with the MATH dataset. In Joaquin Vanschoren and Sai-Kit Yeung (eds.), Proceedings of the Neural Information Processing Systems Track on Datasets and Benchmarks 1, NeurIPS Datasets and Benchmarks 2021, December 2021, virtual, 2021. URL https://datasets-benchmarks-proceedings.neurips.cc/paper/2021/ hash/be83ab3ecd0db773eb2dc1b0a17836a1-Abstract-round2.html.}, } @article{arxiv-2604.00554v1.r10, author = {Hochreiter, S}, title = {{Long Short-term Memory}}, year = {1997}, note = {S Hochreiter. 1997. Long Short-term Memory. Neural Computation MIT-Press (1997).}, } @misc{arxiv-2604.00554v1.r11, author = {Hu, E.J. and Shen, Y. and Wallis, P. and Allen-Zhu, Z. and Li, Y. and Wang, S. and Wang, L. and Chen, W.}, title = {{Lora: Low-rank adaptation of large language models}}, year = {2021}, url = {https://arxiv.org/abs/2106.09685}, note = {E.J. Hu, Y. Shen, P. Wallis, Z. Allen-Zhu, Y. Li, S. Wang, L. Wang, and W. Chen. 2021. Lora: Low-rank adaptation of large language models. arXiv preprint (2021). arXiv:2106.09685}, } @misc{arxiv-2601.22554v1.r11, author = {Hu, Jiewen and Zhu, Thomas and Welleck, Sean}, title = {{miniCTX: Neural Theorem Proving with (Long-)Contexts}}, year = {2025}, note = {Jiewen Hu, Thomas Zhu, and Sean Welleck. miniCTX: Neural Theorem Proving with (Long-)Contexts. In The Thirteenth International Conference on Learning Representations, 2025. URL https://openre view.net/forum?id=KIgaAqEFHW.}, } @misc{arxiv-2406.01940v2.r21, author = {Huang, Daniel and Dhariwal, Prafulla and Song, Dawn and Sutskever, Ilya}, title = {{Gamepad: A learning environment for theorem proving}}, year = {2019}, url = {https://openreview.net/forum?id=r1xwKoR9Y7}, note = {Daniel Huang, Prafulla Dhariwal, Dawn Song, and Ilya Sutskever. Gamepad: A learning environment for theorem proving. In 7th International Conference on Learning Representations, ICLR 2019, New Orleans, LA, USA, May 6-9, 2019. OpenReview.net, 2019. URL https://openreview. net/forum?id=r1xwKoR9Y7.}, } @misc{arxiv-2406.01940v2.r22, author = {Huang, Dong and Dai, Jianbo and Weng, Han and Wu, Puzhen and Qing, Yuhao and Zhang, Jie M and Cui, Heming and Guo, Zhijiang}, title = {{Soap: Enhancing efficiency of generated code via self-optimization}}, year = {2024}, url = {https://arxiv.org/abs/2405.15189}, note = {Dong Huang, Jianbo Dai, Han Weng, Puzhen Wu, Yuhao Qing, Jie M Zhang, Heming Cui, and Zhijiang Guo. Soap: Enhancing efficiency of generated code via self-optimization. arXiv preprint arXiv:2405.15189, 2024a.}, } @misc{arxiv-2003.08005v1.r28, author = {Huang, J. and Rathod, V. and Sun, C. and Zhu, M. and Korattikara, A. and Fathi, A. and Fischer, I. and Wojna, Z. and Song, Y. and Guadarrama, S.}, title = {{Speed/accuracy trade-offs for modern convolutional object detectors}}, year = {2017}, note = {J. Huang, V. Rathod, C. Sun, M. Zhu, A. Korattikara, A. Fathi, I. Fischer, Z. Wojna, Y. Song, S. Guadarrama et al., “Speed/accuracy trade-offs for modern convolutional object detectors,” in Proceedings of the IEEE conference on computer vision and pattern recognition, 2017, pp. 7310– 7311.}, } @article{arxiv-2604.00554v1.r12, author = {Huang, Lei and Yu, Weijiang and Ma, Weitao and Zhong, Weihong and Feng, Zhangyin and Wang, Haotian and Chen, Qianglong and Peng, Weihua and Feng, Xiaocheng and Qin, Bing}, title = {{A survey on hallucination in large language models: Principles, taxonomy, challenges, and open questions}}, year = {2023}, note = {Lei Huang, Weijiang Yu, Weitao Ma, Weihong Zhong, Zhangyin Feng, Haotian Wang, Qianglong Chen, Weihua Peng, Xiaocheng Feng, Bing Qin, et al. 2023. A survey on hallucination in large language models: Principles, taxonomy, chal- lenges, and open questions. ACM Transactions on Information Systems (2023).}, } @misc{arxiv-2406.01940v2.r23, author = {Huang, Yinya and Lin, Xiaohan and Liu, Zhengying and Cao, Qingxing and Xin, Huajian and Wang, Haiming and Li, Zhenguo and Song, Linqi and Liang, Xiaodan}, title = {{MUSTARD: mastering uniform synthesis of theorem and proof data}}, year = {2024}, doi = {10.48550/arXiv.2402.08957}, url = {https://doi.org/10.48550/arXiv.2402.08957}, note = {Yinya Huang, Xiaohan Lin, Zhengying Liu, Qingxing Cao, Huajian Xin, Haiming Wang, Zhenguo Li, Linqi Song, and Xiaodan Liang. MUSTARD: mastering uniform synthesis of theorem and proof data. CoRR, abs/2402.08957, 2024b. doi: 10.48550/ARXIV.2402.08957. URL https: //doi.org/10.48550/arXiv.2402.08957.}, } @article{arxiv-2601.22554v1.r12, author = {Hubert, Thomas and Mehta, Rishi and Sartran, Laurent and Horv{\'{a}}th, Miklós Z. and Žužić, Goran and Wieser, Eric and Huang, Aja and Schrittwieser, Julian and Schroecker, Yannick and Masoom, Hussain}, title = {{Olympiad-Level Formal Mathematical Reasoning with Reinforcement Learning}}, year = {2025}, doi = {10.1038/s41586-025-09833-y}, url = {https://doi.org/10.1038/s41586-025-09833-y}, note = {Thomas Hubert, Rishi Mehta, Laurent Sartran, Miklós Z. Horv{\'{a}}th, Goran Žužić, Eric Wieser, Aja Huang, Julian Schrittwieser, Yannick Schroecker, Hussain Masoom, et al. Olympiad-Level Formal Mathematical Reasoning with Reinforcement Learning. Nature, 2025. doi: 10.1038/s41586-025-09833-y. URL https://doi.org/10.1038/s41586-025-09833-y.}, } @misc{arxiv-2003.08005v1.r15, author = {Iwatsuki, K. and Sagara, T. and Hara, T. and Aizawa, A.}, title = {{Detecting in-line mathematical expressions in scientific documents}}, year = {2017}, note = {K. Iwatsuki, T. Sagara, T. Hara, and A. Aizawa, “Detecting in-line mathematical expressions in scientific documents,” in Proceedings of the 2017 ACM Symposium on Document Engineering. ACM, 2017, pp. 141–144.}, } @misc{arxiv-2406.01940v2.r18, author = {Jesse Michael Han and Rute, Jason and Wu, Yuhuai and Ayers, Edward W. and Polu, Stanislas}, title = {{Proof artifact co-training for theorem proving with language models}}, year = {2022}, url = {https://openreview.net/forum?id=rpxJc9j04U}, note = {Jesse Michael Han, Jason Rute, Yuhuai Wu, Edward W. Ayers, and Stanislas Polu. Proof artifact co-training for theorem proving with language models. In The Tenth International Conference on Learning Representations, ICLR 2022, Virtual Event, April 25-29, 2022. OpenReview.net, 2022. URL https://openreview.net/forum?id=rpxJc9j04U.}, } @misc{arxiv-2406.01940v2.r25, author = {Jiang, Albert Q. and Sablayrolles, Alexandre and Mensch, Arthur and Bamford, Chris and Devendra Singh Chaplot and Diego de Las Casas and Bressand, Florian and Lengyel, Gianna and Lample, Guillaume and Saulnier, Lucile and L{\'{e}}lio Renard Lavaud and Lachaux, Marie-Anne and Stock, Pierre and Teven Le Scao and Lavril, Thibaut and Wang, Thomas and Lacroix, Timoth{\'{e}}e and William El Sayed}, title = {{Mistral 7b}}, year = {2023}, doi = {10.48550/arXiv.2310.06825}, url = {https://doi.org/10.48550/arXiv.2310.06825}, note = {Albert Q. Jiang, Alexandre Sablayrolles, Arthur Mensch, Chris Bamford, Devendra Singh Chaplot, Diego de Las Casas, Florian Bressand, Gianna Lengyel, Guillaume Lample, Lucile Saulnier, L{\'{e}}lio Renard Lavaud, Marie-Anne Lachaux, Pierre Stock, Teven Le Scao, Thibaut Lavril, Thomas Wang, Timoth{\'{e}}e Lacroix, and William El Sayed. Mistral 7b. CoRR, abs/2310.06825, 2023b. doi: 10.48550/ARXIV.2310.06825. URL https://doi.org/10.48550/arXiv.2310. 06825.}, } @misc{arxiv-2406.01940v2.r24, author = {Jiang, Albert Q. and Li, Wenda and Jamnik, Mateja}, title = {{Multilingual mathematical autoformalization}}, year = {2023}, doi = {10.48550/arXiv.2311.03755}, url = {https://doi.org/10.48550/arXiv.2311.03755}, note = {Albert Q. Jiang, Wenda Li, and Mateja Jamnik. Multilingual mathematical autoformalization. CoRR, abs/2311.03755, 2023a. doi: 10.48550/ARXIV.2311.03755. URL https://doi.org/10. 48550/arXiv.2311.03755.}, } @misc{arxiv-2406.01940v2.r19, author = {John Harrison}, title = {{HOL Light: A tutorial introduction}}, year = {1996}, note = {John Harrison. HOL Light: A tutorial introduction. In Mandayam K. Srivas and Albert John Camilleri (eds.), Formal Methods in Computer-Aided Design, First International Conference, FMCAD ’96, Palo Alto, California, USA, November 6-8, 1996, Proceedings, volume 1166 of Lecture Notes in Computer Science, pp. 265–269. Springer, 1996.}, } @misc{arxiv-2602.16554v1.r18, author = {Joseph Tooby-Smith}, title = {{Heplean: Digitalising high energy physics}}, year = {2024}, url = {https://arxiv.org/abs/2405.08863}, note = {Joseph Tooby-Smith. Heplean: Digitalising high energy physics, 2024. URL https://arxiv. org/abs/2405.08863.}, } @misc{arxiv-2406.01940v2.r27, author = {Jung, Jaehun and Qin, Lianhui and Welleck, Sean and Brahman, Faeze and Bhagavatula, Chandra and Ronan Le Bras and Choi, Yejin}, title = {{Maieutic prompting: Logically consistent reasoning with recursive explanations}}, year = {2022}, doi = {10.18653/v1/2022.emnlp-main.82}, note = {Jaehun Jung, Lianhui Qin, Sean Welleck, Faeze Brahman, Chandra Bhagavatula, Ronan Le Bras, and Yejin Choi. Maieutic prompting: Logically consistent reasoning with recursive explanations. In Yoav Goldberg, Zornitsa Kozareva, and Yue Zhang (eds.), Proceedings of the 2022 Conference on Empirical Methods in Natural Language Processing, EMNLP 2022, Abu Dhabi, United Arab Emirates, December 7-11, 2022, pp. 1266–1279. Association for Computational Linguistics, 2022. doi: 10.18653/V1/2022.EMNLP-MAIN.82. URL https://doi.org/10.18653/ v1/2022.emnlp-main.82. Takeshi Kojima, Shixiang Shane Gu, Machel Reid, Yutaka Matsuo, and Yusuke Iwa- sawa. Large language models are zero-shot reasoners. In Sanmi Koyejo, S. Mo- hamed, A. Agarwal, Danielle Belgrave, K. Cho, and A. Oh (eds.), Advances in Neural Information Processing Systems 35: Annual Conference on Neural Information Process- ing Systems 2022, NeurIPS 2022, New Orleans, LA, USA, November 28 - December 9, 2022, 2022. URL http://papers.nips.cc/paper_files/paper/2022/hash/ 8bb0d291acd4acf06ef112099c16f326-Abstract-Conference.html.}, } @misc{arxiv-2601.22554v1.r13, author = {Kontorovich, Alex and Tao, Terence}, title = {{Prime Number Theorem and More}}, year = {2024}, note = {Alex Kontorovich and Terence Tao. Prime Number Theorem and More, 2024. URL https://github.c om/AlexKontorovich/PrimeNumberTheoremAnd.}, } @misc{arxiv-2604.00554v1.r15, author = {Krizhevsky, A. and Sutskever, I. and Hinton, G.E.}, title = {{Imagenet classification with deep convolutional neural networks}}, year = {2012}, note = {A. Krizhevsky, I. Sutskever, and G.E. Hinton. 2012. Imagenet classification with deep convolutional neural networks. Advances in neural information processing systems 25 (2012).}, } @misc{arxiv-2604.00554v1.r16, author = {Kruse, T. and Kliche, F.}, title = {{Definition extraction from mathematical texts on graph theory in German and English}}, year = {2021}, note = {T. Kruse and F. Kliche. 2021. Definition extraction from mathematical texts on graph theory in German and English. In Proceedings of the 17th Conference on Natural Language Processing (KONVENS 2021). 104–113.}, } @misc{arxiv-2512.09874v3.r12, author = {Kumar, A. and Wang, L.L.}, title = {{Uncovering the new accessibility crisis in scholarly PDFs: Publishing model and platform changes contribute to declining scholarly document accessibility in the last decade}}, year = {2024}, note = {Kumar, A., Wang, L.L.: Uncovering the new accessibility crisis in scholarly PDFs: Publishing model and platform changes contribute to declining scholarly document accessibility in the last decade. In: Proceedings of the 26th International ACM SIGACCESS Conference on Computers and Accessibility (ASSETS) (2024)}, } @misc{arxiv-2602.16554v1.r5, author = {Kumarappan, Adarsh and Tiwari, Mo and Song, Peiyang and Robert Joseph George and Xiao, Chaowei and Anandkumar, Anima}, title = {{LeanAgent: Lifelong Learning for Formal Theorem Proving}}, year = {2025}, url = {http://arxiv.org/abs/2410.06209}, note = {Adarsh Kumarappan, Mo Tiwari, Peiyang Song, Robert Joseph George, Chaowei Xiao, and Anima Anandkumar. LeanAgent: Lifelong Learning for Formal Theorem Proving, March 2025. URL http://arxiv.org/abs/2410.06209. arXiv:2410.06209 [cs].}, } @misc{arxiv-2406.01940v2.r28, author = {Kwon, Woosuk and Li, Zhuohan and Zhuang, Siyuan and Sheng, Ying and Zheng, Lianmin and Cody Hao Yu and Gonzalez, Joseph and Zhang, Hao and Stoica, Ion}, title = {{Efficient memory management for large language model serving with pagedattention}}, year = {2023}, doi = {10.1145/3600006.3613165}, url = {https://doi.org/10.1145/3600006.3613165}, note = {Woosuk Kwon, Zhuohan Li, Siyuan Zhuang, Ying Sheng, Lianmin Zheng, Cody Hao Yu, Joseph Gonzalez, Hao Zhang, and Ion Stoica. Efficient memory management for large language model serving with pagedattention. In Jason Flinn, Margo I. Seltzer, Peter Druschel, Antoine Kaufmann, and Jonathan Mace (eds.), Proceedings of the 29th Symposium on Operating Systems Principles, SOSP 2023, Koblenz, Germany, October 23-26, 2023, pp. 611–626. ACM, 2023. doi: 10.1145/ 3600006.3613165. URL https://doi.org/10.1145/3600006.3613165.}, } @misc{arxiv-2512.09874v3.r13, author = {Labahn, G. and Lank, E. and MacLean, S. and Marzouk, M. and Tausky, D.}, title = {{MathBrush: A system for doing math on pen-based devices}}, year = {2008}, note = {Labahn, G., Lank, E., MacLean, S., Marzouk, M., Tausky, D.: MathBrush: A system for doing math on pen-based devices. In: Proceedings of the Eighth IAPR International Workshop on Document Analysis Systems (DAS). pp. 599–606 (2008)}, } @misc{arxiv-2512.09874v3.r14, author = {Levenshtein, V.I.}, title = {{Binary codes capable of correcting deletions, insertions, and reversals}}, year = {1966}, note = {Levenshtein, V.I.: Binary codes capable of correcting deletions, insertions, and reversals. Soviet Physics Doklady 10(8), 707–710 (1966)}, } @misc{arxiv-2604.00554v1.r17, author = {Levenshtein, V.I.}, title = {{Binary codes capable of correcting deletions, insertions, and reversals}}, year = {1966}, note = {V.I. Levenshtein. 1966. Binary codes capable of correcting deletions, insertions, and reversals. Soviet physics doklady 10, 8 (February 1966), 707–710.}, } @misc{arxiv-2512.09874v3.r15, author = {Li, H. and Dong, Q. and Chen, J. and Su, H. and Zhou, Y. and Ai, Q. and Ye, Z. and Liu, Y.}, title = {{Llms-as-judges: A comprehensive survey on llm-based evaluation methods}}, year = {2024}, note = {Li, H., Dong, Q., Chen, J., Su, H., Zhou, Y., Ai, Q., Ye, Z., Liu, Y.: Llms-as-judges: A comprehensive survey on llm-based evaluation methods. arXiv preprint (2024)}, } @misc{arxiv-2604.00554v1.r18, author = {Li, Junlong and Xu, Yiheng and Lv, Tengchao and Cui, Lei and Zhang, Cha and Wei, Furu}, title = {{Dit: Self-supervised pre-training for document image transformer}}, year = {2022}, note = {Junlong Li, Yiheng Xu, Tengchao Lv, Lei Cui, Cha Zhang, and Furu Wei. 2022. Dit: Self-supervised pre-training for document image transformer. In Proceedings of the 30th ACM International Conference on Multimedia. 3530–3539.}, } @misc{arxiv-2512.09874v3.r16, author = {Li, S. and Huang, J. and Zhuang, J. and Shi, Y. and Cai, X. and Xu, M. and Wang, X. and Zhang, L. and Ke, G. and Cai, H.}, title = {{Scilitllm: How to adapt llms for scientific literature understanding}}, year = {2025}, note = {Li, S., Huang, J., Zhuang, J., Shi, Y., Cai, X., Xu, M., Wang, X., Zhang, L., Ke, G., Cai, H.: Scilitllm: How to adapt llms for scientific literature understanding. In: Pro- ceedings of the Thirteenth International Conference on Learning Representations (ICLR) (2025)}, } @misc{arxiv-2406.01940v2.r30, author = {Li, Wenda and Yu, Lei and Wu, Yuhuai and Paulson, Lawrence C.}, title = {{Isarstep: a benchmark for high-level mathematical reasoning}}, year = {2021}, url = {https://openreview.net/forum?id=Pzj6fzU6wkj}, note = {Wenda Li, Lei Yu, Yuhuai Wu, and Lawrence C. Paulson. Isarstep: a benchmark for high-level mathematical reasoning. In 9th International Conference on Learning Representations, ICLR 2021, Virtual Event, Austria, May 3-7, 2021. OpenReview.net, 2021. URL https://openreview. net/forum?id=Pzj6fzU6wkj.}, } @misc{arxiv-2406.01940v2.r31, author = {Li, Yifei and Lin, Zeqi and Zhang, Shizhuo and Fu, Qiang and Chen, Bei and Lou, Jian-Guang and Chen, Weizhu}, title = {{Making language models better reasoners with step-aware verifier}}, year = {2023}, doi = {10.18653/v1/2023.acl-long.291}, url = {https://doi.org/10.18653/v1/2023.acl-long.291}, note = {Yifei Li, Zeqi Lin, Shizhuo Zhang, Qiang Fu, Bei Chen, Jian-Guang Lou, and Weizhu Chen. Making language models better reasoners with step-aware verifier. In Anna Rogers, Jordan L. Boyd- Graber, and Naoaki Okazaki (eds.), Proceedings of the 61st Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), ACL 2023, Toronto, Canada, July 9-14, 2023, pp. 5315–5333. Association for Computational Linguistics, 2023. doi: 10.18653/V1/2023. ACL-LONG.291. URL https://doi.org/10.18653/v1/2023.acl-long.291.}, } @misc{arxiv-2604.00554v1.r19, author = {Li, Z. and Li, Y. and Liang, Q. and Li, P. and Cheng, Z. and Niu, Y. and Pu, S. and Li, X.}, title = {{End-to-End Compound Table Understanding with Multi-Modal Modeling}}, year = {2022}, note = {Z. Li, Y. Li, Q. Liang, P. Li, Z. Cheng, Y. Niu, S. Pu, and X. Li. 2022. End-to-End Compound Table Understanding with Multi-Modal Modeling. In Proceedings of the 30th ACM International Conference on Multimedia. 4112–4121.}, } @misc{arxiv-2602.16554v1.r6, author = {Li, Zenan and Wu, Yifan and Li, Zhaoyu and Wei, Xinming and Zhang, Xian and Yang, Fan and Ma, Xiaoxing}, year = {2024}, url = {https://openreview.net/forum?id=8ihVBYpMV4}, note = {Zenan Li, Yifan Wu, Zhaoyu Li, Xinming Wei, Xian Zhang, Fan Yang, and Xiaoxing Ma. Autofor- malize Mathematical Statements by Symbolic Equivalence and Semantic Consistency. November 2024. URL https://openreview.net/forum?id=8ihVBYpMV4.}, } @misc{arxiv-2003.08005v1.r29, author = {Liao, M. and Shi, B. and Bai, X. and Wang, X. and Liu, W.}, title = {{Textboxes: A fast text detector with a single deep neural network}}, year = {2017}, note = {M. Liao, B. Shi, X. Bai, X. Wang, and W. Liu, “Textboxes: A fast text detector with a single deep neural network,” in Thirty-First AAAI Conference on Artificial Intelligence, 2017.}, } @misc{arxiv-2406.01940v2.r32, author = {Lightman, Hunter and Kosaraju, Vineet and Burda, Yuri and Edwards, Harrison and Baker, Bowen and Lee, Teddy and Leike, Jan and Schulman, John and Sutskever, Ilya and Cobbe, Karl}, title = {{Let’s verify step by step}}, year = {2024}, url = {https://openreview.net/forum?id=v8L0pN6EOi}, note = {Hunter Lightman, Vineet Kosaraju, Yuri Burda, Harrison Edwards, Bowen Baker, Teddy Lee, Jan Leike, John Schulman, Ilya Sutskever, and Karl Cobbe. Let’s verify step by step. In The Twelfth International Conference on Learning Representations, 2024. URL https://openreview. net/forum?id=v8L0pN6EOi.}, } @misc{arxiv-2003.08005v1.r6, author = {Lin, X. and Gao, L. and Tang, Z. and Lin, X. and Hu, X.}, title = {{Mathematical formula identification in pdf documents}}, year = {2011}, note = {X. Lin, L. Gao, Z. Tang, X. Lin, and X. Hu, “Mathematical formula identification in pdf documents,” in 2011 International Conference on Document Analysis and Recognition. IEEE, 2011, pp. 1419–1423.}, } @misc{arxiv-2003.08005v1.r16, author = {Lin, X. and Gao, L. and Tang, Z. and Hu, X. and Lin, X.}, title = {{Identification of embedded mathematical formulas in pdf documents using svm}}, year = {2012}, note = {X. Lin, L. Gao, Z. Tang, X. Hu, and X. Lin, “Identification of embedded mathematical formulas in pdf documents using svm,” in Document Recognition and Retrieval XIX, vol. 8297. International Society for Optics and Photonics, 2012, p. 82970D.}, } @misc{arxiv-2601.22554v1.r15, author = {Lin, Yong and Tang, Shange and Lyu, Bohan and Yang, Ziran and Chung, Jui-Hui and Zhao, Haoyu and Jiang, Lai and Geng, Yihan and Ge, Jiawei and Sun, Jingruo}, title = {{Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction}}, year = {2025}, doi = {10.48550/arXiv.2508.03613}, url = {https://doi.org/10.48550/arXiv.2508.03613}, note = {Yong Lin, Shange Tang, Bohan Lyu, Ziran Yang, Jui-Hui Chung, Haoyu Zhao, Lai Jiang, Yihan Geng, Jiawei Ge, Jingruo Sun, et al. Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction. arXiv preprint, 2025. doi: 10.48550/arXiv.2508.03613. URL https://doi.org/10.48550/arXiv.2508.03613.}, } @misc{arxiv-2602.16554v1.r7, author = {Lin, Yong and Tang, Shange and Lyu, Bohan and Yang, Ziran and Chung, Jui-Hui and Zhao, Haoyu and Jiang, Lai and Geng, Yihan and Ge, Jiawei and Sun, Jingruo and Wu, Jiayun and Gesi, Jiri and Lu, Ximing and Acuna, David and Yang, Kaiyu and Lin, Hongzhou and Choi, Yejin and Chen, Danqi and Arora, Sanjeev and Jin, Chi}, title = {{Goedel-prover-v2: Scaling formal theorem proving with scaffolded data synthesis and self-correction}}, year = {2025}, url = {https://arxiv.org/abs/2508.03613}, note = {Yong Lin, Shange Tang, Bohan Lyu, Ziran Yang, Jui-Hui Chung, Haoyu Zhao, Lai Jiang, Yihan Geng, Jiawei Ge, Jingruo Sun, Jiayun Wu, Jiri Gesi, Ximing Lu, David Acuna, Kaiyu Yang, Hongzhou Lin, Yejin Choi, Danqi Chen, Sanjeev Arora, and Chi Jin. Goedel-prover-v2: Scaling formal theorem proving with scaffolded data synthesis and self-correction, 2025. URL https: //arxiv.org/abs/2508.03613.}, } @misc{arxiv-2601.22554v1.r14, author = {Lin, Yong and Tang, Shange and Lyu, Bohan and Wu, Jiayun and Lin, Hongzhou and Yang, Kaiyu and Li, Jia and Xia, Mengzhou and Chen, Danqi and Arora, Sanjeev}, title = {{Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving}}, year = {2025}, doi = {10.48550/arXiv.2502.07640}, url = {https://arxiv.org/abs/2502.07640}, note = {Yong Lin, Shange Tang, Bohan Lyu, Jiayun Wu, Hongzhou Lin, Kaiyu Yang, Jia Li, Mengzhou Xia, Danqi Chen, Sanjeev Arora, et al. Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving. arXiv preprint, 2025. doi: 10.48550/arXiv.2502.07640. URL https://doi.org/10.48550/arX iv.2502.07640.}, } @misc{arxiv-2406.01940v2.r33, author = {Liu, Chengwu and Shen, Jianhao and Xin, Huajian and Liu, Zhengying and Yuan, Ye and Wang, Haiming and Ju, Wei and Zheng, Chuanyang and Yin, Yichun and Li, Lin and Zhang, Ming and Liu, Qun}, title = {{FIMO: A challenge formal dataset for automated theorem proving}}, year = {2023}, doi = {10.48550/arXiv.2309.04295}, url = {https://doi.org/10.48550/arXiv.2309.04295}, note = {Chengwu Liu, Jianhao Shen, Huajian Xin, Zhengying Liu, Ye Yuan, Haiming Wang, Wei Ju, Chuanyang Zheng, Yichun Yin, Lin Li, Ming Zhang, and Qun Liu. FIMO: A challenge formal dataset for automated theorem proving. CoRR, abs/2309.04295, 2023a. doi: 10.48550/ARXIV. 2309.04295. URL https://doi.org/10.48550/arXiv.2309.04295.}, } @misc{arxiv-2406.01940v2.r34, author = {Liu, Chengwu and Shen, Jianhao and Xin, Huajian and Liu, Zhengying and Yuan, Ye and Wang, Haiming and Ju, Wei and Zheng, Chuanyang and Yin, Yichun and Li, Lin}, title = {{Fimo: A challenge formal dataset for automated theorem proving}}, year = {2023}, url = {https://arxiv.org/abs/2309.04295}, note = {Chengwu Liu, Jianhao Shen, Huajian Xin, Zhengying Liu, Ye Yuan, Haiming Wang, Wei Ju, Chuanyang Zheng, Yichun Yin, Lin Li, et al. Fimo: A challenge formal dataset for automated theorem proving. arXiv preprint arXiv:2309.04295, 2023b.}, } @misc{arxiv-2602.16554v1.r8, author = {Liu, Junqi and Zhou, Zihao and Zhu, Zekai and Marco Dos Santos and He, Weikun and Liu, Jiawei and Wang, Ran and Xie, Yunzhou and Zhao, Junqiao and Wang, Qiufeng and Zhi, Lihong and Li, Jia and Li, Wenda}, title = {{Numina-lean-agent: An open and general agentic reasoning system for formal mathematics}}, year = {2026}, url = {https://arxiv.org/abs/2601.14027}, note = {Junqi Liu, Zihao Zhou, Zekai Zhu, Marco Dos Santos, Weikun He, Jiawei Liu, Ran Wang, Yunzhou Xie, Junqiao Zhao, Qiufeng Wang, Lihong Zhi, Jia Li, and Wenda Li. Numina-lean-agent: An open and general agentic reasoning system for formal mathematics, 2026. URL https: //arxiv.org/abs/2601.14027.}, } @misc{arxiv-2602.16554v1.r9, author = {Liu, Qi and Zheng, Xinhao and Lu, Xudong and Cao, Qinxiang and Yan, Junchi}, title = {{RETHINKING AND IMPROVING AUTOFORMALIZATION: TOWARDS A FAITHFUL METRIC AND A DEPENDENCY RETRIEVAL-BASED APPROACH}}, year = {2025}, note = {Qi Liu, Xinhao Zheng, Xudong Lu, Qinxiang Cao, and Junchi Yan. RETHINKING AND IMPROV- ING AUTOFORMALIZATION: TOWARDS A FAITHFUL METRIC AND A DEPENDENCY RETRIEVAL-BASED APPROACH. 2025.}, } @misc{arxiv-2003.08005v1.r3, author = {Liu, W. and Anguelov, D. and Erhan, D. and Szegedy, C. and Reed, S. and Fu, C.-Y. and Berg, A. C.}, title = {{SSD: Single shot multibox detector}}, year = {2016}, note = {W. Liu, D. Anguelov, D. Erhan, C. Szegedy, S. Reed, C.-Y. Fu, and A. C. Berg, “SSD: Single shot multibox detector,” in European conference on computer vision. Springer, 2016, pp. 21–37.}, } @misc{arxiv-2512.09874v3.r17, author = {Liu, Y. and Yuan, X. and Zhang, H. and Gao, Z. and Zhu, B. and Peng, X. and Lin, Z. and Liu, Q. and Jin, L. and Bai, X.}, title = {{Monkeyocr: Document parsing with a structure-recognition-relation triplet paradigm}}, year = {2025}, note = {Liu, Y., Yuan, X., Zhang, H., Gao, Z., Zhu, B., Peng, X., Lin, Z., Liu, Q., Jin, L., Bai, X.: Monkeyocr: Document parsing with a structure-recognition-relation triplet paradigm. arXiv preprint (2025)}, } @misc{arxiv-2512.09874v3.r19, author = {Lo, K. and Wang, L.L. and Neumann, M. and Kinney, R. and Weld, D.}, title = {{S2ORC: The semantic scholar open research corpus}}, year = {2020}, note = {Lo, K., Wang, L.L., Neumann, M., Kinney, R., Weld, D.: S2ORC: The semantic scholar open research corpus. In: Proceedings of the 58th Annual Meeting of the Association for Computational Linguistics (ACL). pp. 4969–4983 (2020)}, } @misc{arxiv-2512.09874v3.r20, author = {Lopez, P.}, title = {{Grobid: Combining automatic bibliographic data recognition and term extraction for scholarship publications}}, year = {2009}, note = {Lopez, P.: Grobid: Combining automatic bibliographic data recognition and term extraction for scholarship publications. In: Proceedings of the 13th European Con- ference on Research and Advanced Technology for Digital Libraries (ECDL). pp. 473–474 (2009)}, } @misc{arxiv-2604.00554v1.r22, author = {Louis Brul{\'{e}} Naudet}, title = {{Maxine-7B-0401-stock, an xtraordinary 7B model}}, year = {2024}, url = {https://huggingface.co/louisbrulenaudet/Maxine-7B-0401-stock}, note = {Louis Brul{\'{e}} Naudet. 2024. Maxine-7B-0401-stock, an xtraordinary 7B model. https://huggingface.co/louisbrulenaudet/Maxine-7B-0401-stock}, } @misc{arxiv-2406.01940v2.r35, author = {Lu, Jianqiao and Zhong, Wanjun and Huang, Wenyong and Wang, Yufei and Mi, Fei and Wang, Baojun and Wang, Weichao and Shang, Lifeng and Liu, Qun}, title = {{SELF: language-driven self-evolution for large language model}}, year = {2023}, doi = {10.48550/arXiv.2310.00533}, url = {https://doi.org/10.48550/arXiv.2310.00533}, note = {Jianqiao Lu, Wanjun Zhong, Wenyong Huang, Yufei Wang, Fei Mi, Baojun Wang, Weichao Wang, Lifeng Shang, and Qun Liu. SELF: language-driven self-evolution for large language model. CoRR, abs/2310.00533, 2023. doi: 10.48550/ARXIV.2310.00533. URL https://doi.org/ 10.48550/arXiv.2310.00533.}, } @misc{arxiv-2406.01940v2.r36, author = {Lu, Jianqiao and Dou, Zhiyang and Wang, Hongru and Cao, Zeyu and Dai, Jianbo and Wan, Yingjia and Huang, Yinya and Guo, Zhijiang}, title = {{Autocv: Empowering reasoning with automated process labeling via confidence variation}}, year = {2024}, note = {Jianqiao Lu, Zhiyang Dou, Hongru Wang, Zeyu Cao, Jianbo Dai, Yingjia Wan, Yinya Huang, and Zhijiang Guo. Autocv: Empowering reasoning with automated process labeling via confidence variation, 2024a.}, } @misc{arxiv-2406.01940v2.r37, author = {Lu, Jianqiao and Wan, Yingjia and Huang, Yinya and Xiong, Jing and Liu, Zhengying and Guo, Zhijiang}, title = {{Formalalign: Automated alignment evaluation for autoformalization}}, year = {2024}, note = {Jianqiao Lu, Yingjia Wan, Yinya Huang, Jing Xiong, Zhengying Liu, and Zhijiang Guo. Formalalign: Automated alignment evaluation for autoformalization. 2024b.}, } @misc{arxiv-2406.01940v2.r38, author = {Lu, Jianqiao and Zhong, Wanjun and Wang, Yufei and Guo, Zhijiang and Zhu, Qi and Huang, Wenyong and Wang, Yanlin and Mi, Fei and Wang, Baojun and Wang, Yasheng}, title = {{Yoda: Teacher-student progressive learning for language models}}, year = {2024}, url = {https://arxiv.org/abs/2401.15670}, note = {Jianqiao Lu, Wanjun Zhong, Yufei Wang, Zhijiang Guo, Qi Zhu, Wenyong Huang, Yanlin Wang, Fei Mi, Baojun Wang, Yasheng Wang, et al. Yoda: Teacher-student progressive learning for language models. arXiv preprint arXiv:2401.15670, 2024c.}, } @misc{arxiv-2406.01940v2.r39, author = {Ma, Qianli and Zhou, Haotian and Liu, Tingkai and Yuan, Jianbo and Liu, Pengfei and You, Yang and Yang, Hongxia}, title = {{Let’s reward step by step: Step-level reward model as the navigators for reasoning}}, year = {2023}, doi = {10.48550/arXiv.2310.10080}, url = {https://doi.org/10.48550/arXiv.2310.10080}, note = {Qianli Ma, Haotian Zhou, Tingkai Liu, Jianbo Yuan, Pengfei Liu, Yang You, and Hongxia Yang. Let’s reward step by step: Step-level reward model as the navigators for reasoning. CoRR, abs/2310.10080, 2023. doi: 10.48550/ARXIV.2310.10080. URL https://doi.org/10. 48550/arXiv.2310.10080.}, } @misc{arxiv-2604.00554v1.r20, author = {Ma, Zhiwei and Santo, Javier E and Lackey, Greg and Viswanathan, Hari and O’Malley, Daniel}, title = {{Information Extraction from Historical Well Records Using A Large Language Model}}, year = {2024}, url = {https://arxiv.org/abs/2405.05438}, note = {Zhiwei Ma, Javier E Santo, Greg Lackey, Hari Viswanathan, and Daniel O’Malley. 2024. Information Extraction from Historical Well Records Using A Large Lan- guage Model. arXiv preprint arXiv:2405.05438 (2024).}, } @misc{arxiv-2003.08005v1.r5, author = {Mahdavi, M. and Zanibbi, R. and Mouchere, H. and Garain, U.}, title = {{ICDAR 2019 CROHME + TFD: Competition on recognition of handwritten mathematical expressions and typeset formula detection}}, year = {2019}, note = {M. Mahdavi, R. Zanibbi, H. Mouchere, and U. Garain, “ICDAR 2019 CROHME + TFD: Competition on recognition of handwritten mathematical expressions and typeset formula detection,” in ICDAR 2019). IEEE.}, } @misc{arxiv-2003.08005v1.r7, author = {Mahdavi, M. and Condon, M. and Davila, K. and Zanibbi, R.}, title = {{LPGA: Line-of-sight parsing with graph-based attention for math formula recognition}}, year = {2019}, note = {M. Mahdavi, M. Condon, K. Davila, and R. Zanibbi, “LPGA: Line-of-sight parsing with graph-based attention for math formula recognition,” in Proc. International Conference on Document Analysis and Recognition. Sydney, Australia: IAPR, September 2019, pp. 647– 654.}, } @misc{arxiv-2003.08005v1.r31, author = {Mali, P.}, title = {{Scanning single shot detector for math in document images}}, year = {2019}, note = {P. Mali, “Scanning single shot detector for math in document images,” Master’s thesis, Rochester Institute of Technology, Rochester, NY, USA, August 2019.}, } @article{arxiv-2406.01940v2.r50, title = {{Mastering the game of go with deep neural networks and tree search}}, year = {2016}, doi = {10.1038/nature16961}, url = {https://doi.org/10.1038/nature16961}, note = {David Silver, Aja Huang, Chris J. Maddison, Arthur Guez, Laurent Sifre, George van den Driess- che, Julian Schrittwieser, Ioannis Antonoglou, Vedavyas Panneershelvam, Marc Lanctot, Sander Dieleman, Dominik Grewe, John Nham, Nal Kalchbrenner, Ilya Sutskever, Timothy P. Lillicrap, Madeleine Leach, Koray Kavukcuoglu, Thore Graepel, and Demis Hassabis. Mastering the game of go with deep neural networks and tree search. Nature, 529(7587):484–489, 2016. doi: 10.1038/NATURE16961. URL https://doi.org/10.1038/nature16961.}, } @misc{arxiv-2602.16554v1.r10, author = {Meiburg, Alex and Lessa, Leonardo A and Soldati, Rodolfo R}, title = {{A formalization of the generalized quantum stein’s lemma in lean}}, year = {2025}, url = {https://arxiv.org/abs/2510.08672}, note = {Alex Meiburg, Leonardo A Lessa, and Rodolfo R Soldati. A formalization of the generalized quantum stein’s lemma in lean. arXiv preprint arXiv:2510.08672, 2025.}, } @misc{arxiv-2406.01940v2.r41, author = {Meta}, title = {{Introducing meta llama 3: The most capable openly available llm to date}}, year = {2024}, url = {https://ai.meta.com/blog/meta-llama-3/}, note = {Meta. Introducing meta llama 3: The most capable openly available llm to date, 2024. URL https://ai.meta.com/blog/meta-llama-3/.}, } @article{arxiv-2604.00554v1.r21, author = {Mihaljević, Helena and Santamaría, Lucía}, title = {{Authorship in top-ranked mathematical and physical journals: Role of gender on self-perceptions and bibliographic evidence}}, year = {2020}, doi = {10.1162/qss_a_00090}, note = {Helena Mihaljević and Lucía Santamaría. 2020. Authorship in top-ranked mathematical and physical journals: Role of gender on self-perceptions and bibliographic evidence. Quantitative Science Studies 1, 4 (2020), 1468–1492. doi:10.1162/qss_a_00090}, } @misc{arxiv-2406.01940v2.r42, author = {Mikula, Maciej and Antoniak, Szymon and Tworkowski, Szymon and Albert Qiaochu Jiang and Jin Peng Zhou and Szegedy, Christian and Kucinski, Lukasz and Milos, Piotr and Wu, Yuhuai}, year = {2023}, doi = {10.48550/arXiv.2303.04488}, url = {https://doi.org/10.48550/arXiv.2303.04488}, note = {Maciej Mikula, Szymon Antoniak, Szymon Tworkowski, Albert Qiaochu Jiang, Jin Peng Zhou, Christian Szegedy, Lukasz Kucinski, Piotr Milos, and Yuhuai Wu. Magnushammer: A transformer- based approach to premise selection. CoRR, abs/2303.04488, 2023. doi: 10.48550/ARXIV.2303. 04488. URL https://doi.org/10.48550/arXiv.2303.04488.}, } @article{milnorlink.r1, year = {1952}, note = {CHEN, Kuo-TSAI, Isotopy invariants of links, Ann. of Math. 56 (1952) pp. 343-353.}, } @article{milnorlink.r2, year = {1945}, note = {Fox, R. H., Bull. Amer. Math. Soc. 51 (1945), Abstract 140, pg. 526.}, } @article{milnorlink.r3, year = {1953}, note = {Fox, R. H., Free differential calculus, Ann. of Math. 57 (1953) pp. 547-560.}, } @misc{milnorlink.r4, year = {1932}, note = {REIDEMEISTER, K., Knotentheorie, Julius Springer, Berlin, 1932.}, } @misc{arxiv-2406.01940v2.r43, author = {Mukherjee, Subhabrata and Mitra, Arindam and Jawahar, Ganesh and Agarwal, Sahaj and Palangi, Hamid and Awadallah, Ahmed}, title = {{Orca: Progressive learning from complex explanation traces of GPT-4}}, year = {2023}, doi = {10.48550/arXiv.2306.02707}, url = {https://doi.org/10.48550/arXiv.2306.02707}, note = {Subhabrata Mukherjee, Arindam Mitra, Ganesh Jawahar, Sahaj Agarwal, Hamid Palangi, and Ahmed Awadallah. Orca: Progressive learning from complex explanation traces of GPT-4. CoRR, abs/2306.02707, 2023. doi: 10.48550/ARXIV.2306.02707. URL https://doi.org/10. 48550/arXiv.2306.02707.}, } @misc{arxiv-2602.16554v1.r12, author = {Murphy, Logan and Yang, Kaiyu and Sun, Jialiang and Li, Zhaoyu and Anandkumar, Anima and Si, Xujie}, year = {2024}, url = {http://arxiv.org/abs/2405.17216}, note = {Logan Murphy, Kaiyu Yang, Jialiang Sun, Zhaoyu Li, Anima Anandkumar, and Xujie Si. Autofor- malizing Euclidean Geometry, May 2024. URL http://arxiv.org/abs/2405.17216. arXiv:2405.17216 [cs].}, } @misc{arxiv-2003.08005v1.r22, author = {Nagy, G. and Seth, S.}, title = {{Hierarchical representation of optically scanned documents}}, year = {1984}, note = {G. Nagy and S. Seth, “Hierarchical representation of optically scanned documents,” in Proc. Seventh Int’l Conf. Pattern Recognition, Montreal, Canada, 1984, pp. 347–349.}, } @misc{arxiv-2406.01940v2.r44, author = {Nawrocki, Wojciech and Ayers, Edward W. and Ebner, Gabriel}, title = {{An extensible user interface for lean 4}}, year = {2023}, doi = {10.4230/LIPIcs.ITP.2023.24}, url = {https://doi.org/10.4230/LIPIcs.ITP.2023.24}, note = {Wojciech Nawrocki, Edward W. Ayers, and Gabriel Ebner. An extensible user interface for lean 4. In Adam Naumowicz and Ren{\'{e}} Thiemann (eds.), 14th International Conference on Interactive Theorem Proving, ITP 2023, July 31 to August 4, 2023, Bia{\l}ystok, Poland, volume 268 of LIPIcs, pp. 24:1–24:20. Schloss Dagstuhl - Leibniz-Zentrum f{\"u}r Informatik, 2023. doi: 10.4230/LIPICS. ITP.2023.24. URL https://doi.org/10.4230/LIPIcs.ITP.2023.24.}, } @article{arxiv-2003.08005v1.r4, author = {Ohyama, W. and Suzuki, M. and Uchida, S.}, title = {{Detecting mathematical expressions in scientific document images using a u-net trained on a diverse dataset}}, year = {2019}, note = {W. Ohyama, M. Suzuki, and S. Uchida, “Detecting mathematical expressions in scientific document images using a u-net trained on a diverse dataset,” IEEE Access, vol. 7, pp. 144 030–144 042, 2019.}, } @misc{arxiv-2406.01940v2.r45, author = {OpenAI}, title = {{GPT-3.5 Turbo}}, year = {2023}, url = {https://platform.openai.com/docs/models/gpt-3-5}, note = {OpenAI. GPT-3.5 Turbo, 2023. URL https://platform.openai.com/docs/models/ gpt-3-5.}, } @misc{arxiv-2512.09874v3.r26, author = {Ouyang, L. and Qu, Y. and Zhou, H. and Zhu, J. and Zhang, R. and Lin, Q. and Wang, B. and Zhao, Z. and Jiang, M. and Zhao, X. and Shi, J. and Wu, F. and Chu, P. and Liu, M. and Li, Z. and Xu, C. and Zhang, B. and Shi, B. and Tu, Z. and He, C.}, title = {{Omnidocbench: Benchmarking diverse pdf document parsing with comprehensive annotations}}, year = {2025}, note = {Ouyang, L., Qu, Y., Zhou, H., Zhu, J., Zhang, R., Lin, Q., Wang, B., Zhao, Z., Jiang, M., Zhao, X., Shi, J., Wu, F., Chu, P., Liu, M., Li, Z., Xu, C., Zhang, B., Shi, B., Tu, Z., He, C.: Omnidocbench: Benchmarking diverse pdf document parsing with comprehensive annotations. In: Proceedings of the IEEE/CVF Conference on Computer Vision and Pattern Recognition (CVPR). pp. 24838–24848 (2025)}, } @misc{arxiv-2406.01940v2.r46, author = {Ouyang, Long and Wu, Jeffrey and Jiang, Xu and Almeida, Diogo and Wainwright, Carroll L. and Mishkin, Pamela and Zhang, Chong and Agarwal, Sandhini and Slama, Katarina and Ray, Alex and Schulman, John and Hilton, Jacob and Kelton, Fraser and Miller, Luke and Simens, Maddie and Askell, Amanda and Welinder, Peter and Christiano, Paul F. and Leike, Jan and Lowe, Ryan}, title = {{Training language models to follow instructions with human feedback}}, year = {2022}, url = {http://papers.nips.cc/paper_files/paper/2022/hash/b1efde53be364a73914f58805a001731-Abstract-Conference.html}, note = {Long Ouyang, Jeffrey Wu, Xu Jiang, Diogo Almeida, Carroll L. Wainwright, Pamela Mishkin, Chong Zhang, Sandhini Agarwal, Katarina Slama, Alex Ray, John Schulman, Jacob Hilton, Fraser Kelton, Luke Miller, Maddie Simens, Amanda Askell, Peter Welinder, Paul F. Christiano, Jan Leike, and Ryan Lowe. Training language models to follow instructions with human feedback. In Sanmi Koyejo, S. Mohamed, A. Agarwal, Danielle Belgrave, K. Cho, and A. Oh (eds.), Advances in Neural Information Processing Systems 35: Annual Conference on Neural Information Processing Systems 2022, NeurIPS 2022, New Orleans, LA, USA, November 28 - December 9, 2022, 2022. URL http://papers.nips.cc/paper_files/paper/2022/hash/ b1efde53be364a73914f58805a001731-Abstract-Conference.html.}, } @misc{arxiv-2604.00554v1.r23, author = {Palm, R.B. and Winther, O. and Laws, F.}, title = {{Cloudscan: A configuration-free invoice analysis system using recurrent neural networks}}, year = {2017}, note = {R.B. Palm, O. Winther, and F. Laws. 2017. Cloudscan: A configuration-free invoice analysis system using recurrent neural networks. In 2017 14th IAPR International Conference on Document Analysis and Recognition (ICDAR), Vol. 1. IEEE, 406–413.}, } @article{arxiv-2604.00554v1.r24, author = {Pandey, M. and Arora, M. and Arora, S. and Goyal, C. and Gera, V.K. and Yadav, H.}, title = {{AI-based Integrated Approach for the Development of Intelligent Document Management System (IDMS)}}, year = {2023}, note = {M. Pandey, M. Arora, S. Arora, C. Goyal, V.K. Gera, and H. Yadav. 2023. AI-based Integrated Approach for the Development of Intelligent Document Management System (IDMS). Procedia Computer Science 230 (2023), 725–736.}, } @misc{arxiv-2512.09874v3.r27, author = {Papineni, K. and Roukos, S. and Ward, T. and Zhu, W.J.}, title = {{BLEU: A method for automatic evaluation of machine translation}}, year = {2002}, note = {Papineni, K., Roukos, S., Ward, T., Zhu, W.J.: BLEU: A method for automatic evaluation of machine translation. In: Proceedings of the 40th Annual Meeting of the Association for Computational Linguistics (ACL). pp. 311–318 (2002)}, } @misc{arxiv-2601.22554v1.r16, author = {Patrick Massot}, title = {{leanblueprint: plasTeX Plugin to Build Formalization Blueprints}}, year = {2020}, url = {https://github.com/PatrickMassot/leanblueprint}, note = {Patrick Massot. leanblueprint: plasTeX Plugin to Build Formalization Blueprints, 2020. URL https: //github.com/PatrickMassot/leanblueprint.}, } @misc{arxiv-2602.16554v1.r14, author = {Peng, Zhongyuan and Yao, Yifan and Ma, Kaijing and Guo, Shuyue and Li, Yizhe and Zhang, Yichi and Zhang, Chenchen and Zhang, Yifan and Yu, Zhouliang and Li, Luming and Liu, Minghao and Xia, Yihang and Shen, Jiawei and Wu, Yuchen and Cao, Yixin and Zhang, Zhaoxiang and Huang, Wenhao and Liu, Jiaheng and Zhang, Ge}, title = {{CriticLean: Critic-Guided Reinforcement Learning for Mathematical Formalization}}, year = {2025}, url = {http://arxiv.org/abs/2507.06181}, note = {Zhongyuan Peng, Yifan Yao, Kaijing Ma, Shuyue Guo, Yizhe Li, Yichi Zhang, Chenchen Zhang, Yifan Zhang, Zhouliang Yu, Luming Li, Minghao Liu, Yihang Xia, Jiawei Shen, Yuchen Wu, Yixin Cao, Zhaoxiang Zhang, Wenhao Huang, Jiaheng Liu, and Ge Zhang. CriticLean: Critic-Guided Reinforcement Learning for Mathematical Formalization, July 2025. URL http://arxiv. org/abs/2507.06181. arXiv:2507.06181 [cs].}, } @misc{arxiv-2604.00554v1.r26, author = {Perot, Vincent and Kang, Kai and Luisier, Florian and Su, Guolong and Sun, Xiaoyu and Ramya Sree Boppana and Wang, Zilong and Wang, Zifeng and Mu, Jiaqi and Zhang, Hao}, title = {{Lmdx: Language model-based document information extraction and localization}}, year = {2023}, url = {https://arxiv.org/abs/2309.10952}, note = {Vincent Perot, Kai Kang, Florian Luisier, Guolong Su, Xiaoyu Sun, Ramya Sree Boppana, Zilong Wang, Zifeng Wang, Jiaqi Mu, Hao Zhang, et al. 2023. Lmdx: Language model-based document information extraction and localization. arXiv preprint arXiv:2309.10952 (2023).}, } @misc{arxiv-2003.08005v1.r13, author = {Pfahler, L. and Schill, J. and Morik, K.}, title = {{The search for equations - learning to identify similarities between mathematical expressions}}, year = {2019}, note = {L. Pfahler, J. Schill, and K. Morik, “The search for equations - learning to identify similarities between mathematical expressions,” in Proc. ECML-PKDD, 2019.}, } @misc{arxiv-2512.09874v3.r28, author = {Pfitzmann, B. and Auer, C. and Dolfi, M. and Nassar, A.S. and Staar, P.}, title = {{Doclaynet: A large human-annotated dataset for document-layout analysis}}, year = {2022}, note = {Pfitzmann, B., Auer, C., Dolfi, M., Nassar, A.S., Staar, P.: Doclaynet: A large human-annotated dataset for document-layout analysis. In: Proceedings of the 28th ACM SIGKDD Conference on Knowledge Discovery and Data Mining (KDD). pp. 3743–3751 (2022)}, } @misc{arxiv-2604.00554v1.r27, author = {Pitou, C. and Diatta, J.}, title = {{Textual information extraction in document images guided by a concept lattice}}, year = {2016}, note = {C. Pitou and J. Diatta. 2016. Textual information extraction in document images guided by a concept lattice. (2016).}, } @misc{arxiv-2601.22554v1.r17, author = {Poiroux, Auguste and Bosselut, Antoine and Kunčak, Viktor}, title = {{RLMEval: Evaluating Research-Level Neural Theorem Proving}}, year = {2025}, doi = {10.48550/arXiv.2510.25427}, url = {https://doi.org/10.48550/arXiv.2510.25427}, note = {Auguste Poiroux, Antoine Bosselut, and Viktor Kunčak. RLMEval: Evaluating Research-Level Neural Theorem Proving. In Findings of the Association for Computational Linguistics: EMNLP 2025, 2025. doi: 10.48550/arXiv.2510.25427. URL https://doi.org/10.48550/arXiv.2510.25427.}, } @misc{arxiv-2512.09874v3.r29, author = {Poznanski, J. and Soldaini, L. and Lo, K.}, title = {{olmocr 2: Unit test rewards for document ocr}}, year = {2025}, note = {Poznanski, J., Soldaini, L., Lo, K.: olmocr 2: Unit test rewards for document ocr. arXiv preprint (2025)}, } @misc{arxiv-2604.00554v1.r28, author = {Re, Matteo and Valentini, Giorgio}, year = {2012}, note = {Matteo Re and Giorgio Valentini. 2012. Ensemble methods: a review in Advances in Machine Learning and Data Mining for Astronomy (ed. Kumar, V.) 563–594.}, } @misc{arxiv-2003.08005v1.r27, author = {Redmon, J. and Divvala, S. and Girshick, R. and Farhadi, A.}, title = {{You only look once: Unified, real-time object detection}}, year = {2016}, note = {J. Redmon, S. Divvala, R. Girshick, and A. Farhadi, “You only look once: Unified, real-time object detection,” in Proceedings of the IEEE conference on computer vision and pattern recognition, 2016, pp. 779– 788.}, } @misc{arxiv-2406.01940v2.r47, author = {Reichel, Tom and Henderson, R. Wesley and Touchet, Andrew and Gardner, Andrew and Ringer, Talia}, title = {{Proof repair infrastructure for supervised models: Building a large proof repair dataset}}, year = {2023}, doi = {10.4230/LIPIcs.ITP.2023.26}, url = {https://doi.org/10.4230/LIPIcs.ITP.2023.26}, note = {Tom Reichel, R. Wesley Henderson, Andrew Touchet, Andrew Gardner, and Talia Ringer. Proof repair infrastructure for supervised models: Building a large proof repair dataset. In Adam Naumowicz and Ren{\'{e}} Thiemann (eds.), 14th International Conference on Interactive Theorem Proving, ITP 2023, July 31 to August 4, 2023, Bia{\l}ystok, Poland, volume 268 of LIPIcs, pp. 26:1–26:20. Schloss Dagstuhl - Leibniz-Zentrum f{\"u}r Informatik, 2023. doi: 10.4230/LIPICS.ITP.2023.26. URL https://doi.org/10.4230/LIPIcs.ITP.2023.26.}, } @misc{arxiv-2406.01940v2.r11, author = {R{\'{e}}mi Coulom}, title = {{Efficient selectivity and backup operators in monte-carlo tree search}}, year = {2006}, doi = {10.1007/978-3-540-75538-8_7}, url = {https://doi.org/10.1007/978-3-540-75538-8_7}, note = {R{\'{e}}mi Coulom. Efficient selectivity and backup operators in monte-carlo tree search. In H. Jaap van den Herik, Paolo Ciancarini, and H. H. L. M. Donkers (eds.), Computers and Games, 5th International Conference, CG 2006, Turin, Italy, May 29-31, 2006. Revised Papers, volume 4630 of Lecture Notes in Computer Science, pp. 72–83. Springer, 2006. doi: 10.1007/978-3-540-75538-8\_7. URL https://doi.org/10.1007/978-3-540-75538-8_7.}, } @misc{arxiv-2003.08005v1.r26, author = {Ren, S. and He, K. and Girshick, R. and Sun, J.}, title = {{Faster r-cnn: Towards real-time object detection with region proposal networks}}, year = {2015}, note = {S. Ren, K. He, R. Girshick, and J. Sun, “Faster r-cnn: Towards real-time object detection with region proposal networks,” in Advances in neural information processing systems, 2015, pp. 91–99.}, } @article{arxiv-2604.00554v1.r29, author = {Ren, Shaoqing and He, Kaiming and Girshick, Ross and Sun, Jian}, title = {{Faster R-CNN: Towards real-time object detection with region proposal networks}}, year = {2016}, note = {Shaoqing Ren, Kaiming He, Ross Girshick, and Jian Sun. 2016. Faster R-CNN: Towards real-time object detection with region proposal networks. IEEE transac- tions on pattern analysis and machine intelligence 39, 6 (2016), 1137–1149.}, } @misc{arxiv-2601.22554v1.r18, author = {Ren, Z. Z. and Shao, Zhihong and Song, Junxiao and Xin, Huajian and Wang, Haocheng and Zhao, Wanjia and Zhang, Liyue and Fu, Zhe and Zhu, Qihao and Yang, Dejian}, title = {{DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition}}, year = {2025}, doi = {10.48550/arXiv.2504.21801}, url = {https://doi.org/10.48550/arXiv.2504.21801}, note = {Z. Z. Ren, Zhihong Shao, Junxiao Song, Huajian Xin, Haocheng Wang, Wanjia Zhao, Liyue Zhang, Zhe Fu, Qihao Zhu, Dejian Yang, et al. DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition. arXiv preprint, 2025. doi: 10.48550/arXiv.2504.21801. URL https://doi.org/10.48550/arXiv.2504.21801.}, } @misc{arxiv-2604.00554v1.r14, title = {{Retrieving documents with mathematical content}}, year = {2013}, doi = {10.1145/2484028.2484083}, note = {Shahab Kamali and Frank Wm. Tompa. 2013. Retrieving documents with mathe- matical content. In Proceedings of the 36th International ACM SIGIR Conference on Research and Development in Information Retrieval, SIGIR ’13, Dublin, Ireland - July 28 - August 01, 2013. 353–362. doi:10.1145/2484028.2484083}, } @misc{arxiv-2601.22554v1.r19, author = {Riehl, Emily and Verity, Dominic}, title = {{Infinity Cosmos: A Blueprint for a Formalization of Infinity-Cosmos Theory in Lean}}, year = {2024}, url = {https://github.com/emilyriehl/infinity-cosmos}, note = {Emily Riehl and Dominic Verity. Infinity Cosmos: A Blueprint for a Formalization of Infinity-Cosmos Theory in Lean, 2024. URL https://github.com/emilyriehl/infinity-cosmos.}, } @misc{arxiv-2604.00554v1.r30, author = {Ronneberger, Olaf and Fischer, Philipp and Brox, Thomas}, title = {{U-net: Convolutional networks for biomedical image segmentation}}, year = {2015}, note = {Olaf Ronneberger, Philipp Fischer, and Thomas Brox. 2015. U-net: Convolu- tional networks for biomedical image segmentation. In Medical image computing and computer-assisted intervention–MICCAI 2015: 18th international conference, Munich, Germany, October 5-9, 2015, proceedings, part III 18. Springer, 234–241.}, } @article{arxiv-2512.09874v3.r34, author = {Sain, K. and Dasgupta, A. and Garain, U.}, title = {{EMERS: A tree matching-based performance evaluation of mathematical expression recognition systems}}, year = {2011}, note = {Sain, K., Dasgupta, A., Garain, U.: EMERS: A tree matching-based performance evaluation of mathematical expression recognition systems. International Journal on Document Analysis and Recognition (IJDAR) 14(1), 75–85 (2011)}, } @article{arxiv-2604.00554v1.r31, author = {Schubotz, Moritz and Teschke, Olaf}, title = {{Four decades of TEX at zbMATH}}, year = {2019}, note = {Moritz Schubotz and Olaf Teschke. 2019. Four decades of TEX at zbMATH. Newsletter of the European Mathematical Society (EMS) 6 (2019), 50–52.}, } @misc{arxiv-2406.01940v2.r40, title = {{Self-refine: Iterative refinement with self-feedback}}, year = {2023}, url = {http://papers.nips.cc/paper_files/paper/2023/hash/91edff07232fb1b55a505a9e9f6c0ff3-Abstract-Conference.html}, note = {Aman Madaan, Niket Tandon, Prakhar Gupta, Skyler Hallinan, Luyu Gao, Sarah Wiegr- effe, Uri Alon, Nouha Dziri, Shrimai Prabhumoye, Yiming Yang, Shashank Gupta, Bod- hisattwa Prasad Majumder, Katherine Hermann, Sean Welleck, Amir Yazdanbakhsh, and Peter Clark. Self-refine: Iterative refinement with self-feedback. In Alice Oh, Tristan Naumann, Amir Globerson, Kate Saenko, Moritz Hardt, and Sergey Levine (eds.), Ad- vances in Neural Information Processing Systems 36: Annual Conference on Neural Infor- mation Processing Systems 2023, NeurIPS 2023, New Orleans, LA, USA, December 10 - 16, 2023, 2023. URL http://papers.nips.cc/paper_files/paper/2023/hash/ 91edff07232fb1b55a505a9e9f6c0ff3-Abstract-Conference.html.}, } @misc{arxiv-2406.01940v2.r48, author = {Shao, Zhihong and Wang, Peiyi and Zhu, Qihao and Xu, Runxin and Song, Junxiao and Zhang, Mingchuan and Li, Y. K. and Wu, Y. and Guo, Daya}, title = {{Deepseekmath: Pushing the limits of mathematical reasoning in open language models}}, year = {2024}, doi = {10.48550/arXiv.2402.03300}, url = {https://doi.org/10.48550/arXiv.2402.03300}, note = {Zhihong Shao, Peiyi Wang, Qihao Zhu, Runxin Xu, Junxiao Song, Mingchuan Zhang, Y. K. Li, Y. Wu, and Daya Guo. Deepseekmath: Pushing the limits of mathematical reasoning in open language models. CoRR, abs/2402.03300, 2024. doi: 10.48550/ARXIV.2402.03300. URL https://doi.org/10.48550/arXiv.2402.03300.}, } @misc{arxiv-2406.01940v2.r49, author = {Shinn, Noah and Cassano, Federico and Gopinath, Ashwin and Narasimhan, Karthik and Yao, Shunyu}, year = {2023}, url = {http://papers.nips.cc/paper_files/paper/2023/hash/1b44b878bb782e6954cd888628510e90-Abstract-Conference.html}, note = {Noah Shinn, Federico Cassano, Ashwin Gopinath, Karthik Narasimhan, and Shunyu Yao. Re- flexion: language agents with verbal reinforcement learning. In Alice Oh, Tristan Nau- mann, Amir Globerson, Kate Saenko, Moritz Hardt, and Sergey Levine (eds.), Advances in Neural Information Processing Systems 36: Annual Conference on Neural Informa- tion Processing Systems 2023, NeurIPS 2023, New Orleans, LA, USA, December 10 - 16, 2023, 2023. URL http://papers.nips.cc/paper_files/paper/2023/hash/ 1b44b878bb782e6954cd888628510e90-Abstract-Conference.html.}, } @misc{arxiv-2512.09874v3.r35, author = {Siebenschuh, C. and Hippe, K. and Gokdemir, O. and Brace, A. and Khan, A.M. and Hossain, K. and Babuji, Y. and Chia, N. and Vishwanath, V. and Ramanathan, A.}, year = {2025}, note = {Siebenschuh, C., Hippe, K., Gokdemir, O., Brace, A., Khan, A.M., Hossain, K., Babuji, Y., Chia, N., Vishwanath, V., Ramanathan, A., et al.: Adaparse: An adap- tive parallel pdf parsing and resource scaling engine. In: Proceedings of the 8th Annual Conference on Machine Learning and Systems (MLSys) (2025)}, } @misc{arxiv-2003.08005v1.r23, author = {Simonyan, K. and Zisserman, A.}, title = {{Very deep convolutional networks for large-scale image recognition}}, year = {2014}, url = {https://arxiv.org/abs/1409.1556}, note = {K. Simonyan and A. Zisserman, “Very deep convolutional networks for large-scale image recognition,” arXiv preprint arXiv:1409.1556, 2014.}, } @misc{arxiv-2512.09874v3.r36, author = {Soldaini, L. and Kinney, R. and Bhagia, A. and Schwenk, D. and Atkinson, D. and Authur, R. and Bogin, B. and Chandu, K. and Dumas, J. and Elazar, Y. and Hofmann, V. and Jha, A. and Kumar, S. and Lucy, L. and Lyu, X. and Lambert, N. and Magnusson, I. and Morrison, J. and Muennighoff, N. and Naik, A. and Nam, C. and Peters, M. and Ravichander, A. and Richardson, K. and Shen, Z. and Strubell, E. and Subramani, N. and Tafjord, O. and Walsh, E. and Zettlemoyer, L. and Smith, N. and Hajishirzi, H. and Beltagy, I. and Groeneveld, D. and Dodge, J. and Lo, K.}, title = {{Dolma: an open corpus of three trillion tokens for language model pretraining research}}, year = {2024}, note = {Soldaini, L., Kinney, R., Bhagia, A., Schwenk, D., Atkinson, D., Authur, R., Bogin, B., Chandu, K., Dumas, J., Elazar, Y., Hofmann, V., Jha, A., Kumar, S., Lucy, L., Lyu, X., Lambert, N., Magnusson, I., Morrison, J., Muennighoff, N., Naik, A., Nam, C., Peters, M., Ravichander, A., Richardson, K., Shen, Z., Strubell, E., Subramani, N., Tafjord, O., Walsh, E., Zettlemoyer, L., Smith, N., Hajishirzi, H., Beltagy, I., Groeneveld, D., Dodge, J., Lo, K.: Dolma: an open corpus of three trillion tokens for language model pretraining research. In: Proceedings of the 62nd Annual Meeting of the Association for Computational Linguistics (ACL). pp. 15725–15788 (2024)}, } @misc{arxiv-2604.00554v1.r32, author = {Sun, Y. and Zhou, D. and Lin, C. and He, C. and Ouyang, W. and Zhong, H.S.}, year = {2024}, url = {https://arxiv.org/abs/2403.02127}, note = {Y. Sun, D. Zhou, C. Lin, C. He, W. Ouyang, and H.S. Zhong. 2024. LOCR: Location- Guided Transformer for Optical Character Recognition. arXiv preprint (2024). arXiv:2403.02127}, } @misc{arxiv-2003.08005v1.r30, author = {Suzuki, M. and Tamari, F. and Fukuda, R. and Uchida, S. and Kanahori, T.}, title = {{Infty: an integrated ocr system for mathematical documents}}, year = {2003}, note = {M. Suzuki, F. Tamari, R. Fukuda, S. Uchida, and T. Kanahori, “Infty: an integrated ocr system for mathematical documents,” in Proceedings of the 2003 ACM symposium on Document engineering. ACM, 2003, pp. 95–104.}, } @misc{arxiv-2604.00554v1.r33, author = {Tang, Z. and Zhang, X. and Wan, B. and Wei, F.}, title = {{Mathscale: Scaling instruction tuning for mathematical reasoning}}, year = {2024}, url = {https://arxiv.org/abs/2403.02884}, note = {Z. Tang, X. Zhang, B. Wan, and F. Wei. 2024. Mathscale: Scaling instruction tuning for mathematical reasoning. arXiv preprint (2024). arXiv:2403.02884 https://arxiv.org/abs/2403.02884}, } @misc{arxiv-2602.16554v1.r16, author = {Tarrach, Guillem and Jiang, Albert Q. and Raggi, Daniel and Li, Wenda and Jamnik, Mateja}, title = {{More Details, Please: Improving Autoformalization with More Detailed Proofs}}, year = {2024}, url = {https://openreview.net/forum?id=AkJvzpYMvK}, note = {Guillem Tarrach, Albert Q. Jiang, Daniel Raggi, Wenda Li, and Mateja Jamnik. More Details, Please: Improving Autoformalization with More Detailed Proofs. June 2024. URL https: //openreview.net/forum?id=AkJvzpYMvK.}, } @misc{arxiv-2602.16554v1.r17, author = {The Coq Development Team}, title = {{The Coq Proof Assistant}}, year = {2024}, url = {https://zenodo.org/records/11551307}, note = {The Coq Development Team. The Coq Proof Assistant, June 2024. URL https://zenodo. org/records/11551307. Language: eng.}, } @misc{arxiv-2601.22554v1.r20, author = {The mathlib Community}, title = {{The Lean Mathematical Library}}, year = {2020}, doi = {10.1145/3372885.3373824}, url = {https://doi.org/10.1145/3372885.3373824}, note = {The mathlib Community. The Lean Mathematical Library. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP ’20, pages 367–381. ACM, 2020. doi: 10.1145/3372885.3373824. URL https://doi.org/10.1145/3372885.3373824.}, } @misc{arxiv-2604.00554v1.r34, author = {Tolokin, D.S. and Korobkin, D.M. and Fomenkov, S.A. and Kolesnikov, S.G.}, title = {{The analysis of the graphical representation of mathematical formulas for extending descriptions of physical effects}}, year = {2021}, note = {D.S. Tolokin, D.M. Korobkin, S.A. Fomenkov, and S.G. Kolesnikov. 2021. The analysis of the graphical representation of mathematical formulas for extending descriptions of physical effects. In Journal of Physics: Conference Series, Vol. 1801. IOP Publishing, 012016.}, } @misc{arxiv-2406.01940v2.r52, author = {Uesato, Jonathan and Kushman, Nate and Kumar, Ramana and Song, H. Francis and Siegel, Noah Y. and Wang, Lisa and Creswell, Antonia and Irving, Geoffrey and Higgins, Irina}, year = {2022}, doi = {10.48550/arXiv.2211.14275}, url = {https://doi.org/10.48550/arXiv.2211.14275}, note = {Jonathan Uesato, Nate Kushman, Ramana Kumar, H. Francis Song, Noah Y. Siegel, Lisa Wang, Antonia Creswell, Geoffrey Irving, and Irina Higgins. Solving math word problems with process- and outcome-based feedback. CoRR, abs/2211.14275, 2022. doi: 10.48550/ARXIV.2211.14275. URL https://doi.org/10.48550/arXiv.2211.14275.}, } @misc{arxiv-2406.01940v2.r53, author = {Ullrich, Sebastian and de Moura, Leonardo}, title = {{Counting immutable beans: Reference counting optimized for purely functional programming}}, year = {2019}, url = {http://arxiv.org/abs/1908.05647}, note = {Sebastian Ullrich and Leonardo de Moura. Counting immutable beans: Reference counting optimized for purely functional programming. CoRR, abs/1908.05647, 2019. URL http://arxiv.org/ abs/1908.05647.}, } @misc{arxiv-2406.01940v2.r54, author = {Ullrich, Sebastian and de Moura, Leonardo}, title = {{’do’ unchained: embracing local imperativity in a purely functional language (functional pearl)}}, year = {2022}, doi = {10.1145/3547640}, url = {https://doi.org/10.1145/3547640}, note = {Sebastian Ullrich and Leonardo de Moura. ’do’ unchained: embracing local imperativity in a purely functional language (functional pearl). Proc. ACM Program. Lang., 6(ICFP):512–539, 2022a. doi: 10.1145/3547640. URL https://doi.org/10.1145/3547640.}, } @misc{arxiv-2406.01940v2.r55, author = {Ullrich, Sebastian and de Moura, Leonardo}, title = {{Beyond notations: Hygienic macro expansion for theorem proving languages}}, year = {2022}, note = {Sebastian Ullrich and Leonardo de Moura. Beyond notations: Hygienic macro expansion for theorem proving languages. Logical Methods in Computer Science, 18, 2022b.}, } @misc{arxiv-2604.00554v1.r35, author = {Varshney, Neeraj and Yao, Wenlin and Zhang, Hongming and Chen, Jianshu and Yu, Dong}, title = {{A stitch in time saves nine: Detecting and mitigating hallucinations of llms by validating low-confidence generation}}, year = {2023}, url = {https://arxiv.org/abs/2307.03987}, note = {Neeraj Varshney, Wenlin Yao, Hongming Zhang, Jianshu Chen, and Dong Yu. 2023. A stitch in time saves nine: Detecting and mitigating hallucinations of llms by validating low-confidence generation. arXiv preprint arXiv:2307.03987 (2023).}, } @misc{arxiv-2512.09874v3.r38, author = {Wang, B. and Xu, C. and Zhao, X. and Ouyang, L. and Wu, F. and Zhao, Z. and Xu, R. and Liu, K. and Qu, Y. and Shang, F. and Zhang, B. and Wei, L. and Sui, Z. and Li, W. and Shi, B. and Qiao, Y. and Lin, D. and He, C.}, title = {{Mineru: An open-source solution for precise document content extraction}}, year = {2024}, note = {Wang, B., Xu, C., Zhao, X., Ouyang, L., Wu, F., Zhao, Z., Xu, R., Liu, K., Qu, Y., Shang, F., Zhang, B., Wei, L., Sui, Z., Li, W., Shi, B., Qiao, Y., Lin, D., He, C.: Mineru: An open-source solution for precise document content extraction. arXiv preprint (2024)}, } @misc{arxiv-2512.09874v3.r37, author = {Wang, B. and Wu, F. and Ouyang, L. and Gu, Z. and Zhang, R. and Xia, R. and Shi, B. and Zhang, B. and He, C.}, title = {{Image over text: Transforming formula recognition evaluation with character detection matching}}, year = {2025}, note = {Wang, B., Wu, F., Ouyang, L., Gu, Z., Zhang, R., Xia, R., Shi, B., Zhang, B., He, C.: Image over text: Transforming formula recognition evaluation with character detection matching. In: Proceedings of the IEEE/CVF Conference on Computer Vision and Pattern Recognition (CVPR). pp. 19681–19690 (2025)}, } @misc{arxiv-2601.22554v1.r21, author = {Wang, Haiming and Unsal, Mert and Lin, Xiaohan and Baksys, Mantas and Liu, Junqi and Marco Dos Santos and Sung, Flood and Vinyes, Marina and Ying, Zhenzhe and Zhu, Zekai}, title = {{Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning}}, year = {2025}, doi = {10.48550/arXiv.2504.11354}, url = {https://doi.org/10.48550/arXiv.2504.11354}, note = {Haiming Wang, Mert Unsal, Xiaohan Lin, Mantas Baksys, Junqi Liu, Marco Dos Santos, Flood Sung, Marina Vinyes, Zhenzhe Ying, Zekai Zhu, et al. Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning. arXiv preprint, 2025. doi: 10.48550/arXiv.2504.11354. URL https://doi.org/10.48550/arXiv.2504.11354.}, } @misc{arxiv-2406.01940v2.r56, author = {Wang, Peiyi and Li, Lei and Shao, Zhihong and Xu, R. X. and Dai, Damai and Li, Yifei and Chen, Deli and Wu, Y. and Sui, Zhifang}, title = {{Math-shepherd: Verify and reinforce llms step-by-step without human annotations}}, year = {2023}, doi = {10.48550/arXiv.2312.08935}, url = {https://doi.org/10.48550/arXiv.2312.08935}, note = {Peiyi Wang, Lei Li, Zhihong Shao, R. X. Xu, Damai Dai, Yifei Li, Deli Chen, Y. Wu, and Zhifang Sui. Math-shepherd: Verify and reinforce llms step-by-step without human annotations. CoRR, abs/2312.08935, 2023a. doi: 10.48550/ARXIV.2312.08935. URL https://doi.org/10. 48550/arXiv.2312.08935.}, } @misc{arxiv-2406.01940v2.r57, author = {Wang, Qingxiang and Kaliszyk, Cezary and Urban, Josef}, title = {{First experiments with neural translation of informal to formal mathematics}}, year = {2018}, doi = {10.1007/978-3-319-96812-4_22}, url = {https://doi.org/10.1007/978-3-319-96812-4_22}, note = {Qingxiang Wang, Cezary Kaliszyk, and Josef Urban. First experiments with neural translation of informal to formal mathematics. In Florian Rabe, William M. Farmer, Grant O. Passmore, and Abdou Youssef (eds.), Intelligent Computer Mathematics - 11th International Conference, CICM 2018, Hagenberg, Austria, August 13-17, 2018, Proceedings, volume 11006 of Lecture Notes in Computer Science, pp. 255–270. Springer, 2018. doi: 10.1007/978-3-319-96812-4\_22. URL https://doi.org/10.1007/978-3-319-96812-4_22.}, } @misc{arxiv-2406.01940v2.r58, author = {Wang, Qingxiang and Brown, Chad E. and Kaliszyk, Cezary and Urban, Josef}, title = {{Exploration of neural machine translation in autoformalization of mathematics in mizar}}, year = {2020}, doi = {10.1145/3372885.3373827}, url = {https://doi.org/10.1145/3372885.3373827}, note = {Qingxiang Wang, Chad E. Brown, Cezary Kaliszyk, and Josef Urban. Exploration of neural machine translation in autoformalization of mathematics in mizar. In Jasmin Blanchette and Catalin Hritcu (eds.), Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020, pp. 85–98. ACM, 2020. doi: 10.1145/3372885.3373827. URL https://doi.org/10.1145/3372885.3373827.}, } @misc{arxiv-2406.01940v2.r59, author = {Wang, Xuezhi and Wei, Jason and Schuurmans, Dale and Le, Quoc V. and Chi, Ed H. and Narang, Sharan and Chowdhery, Aakanksha and Zhou, Denny}, title = {{Self-consistency improves chain of thought reasoning in language models}}, year = {2023}, url = {https://openreview.net/pdf?id=1PL1NIMMrw}, note = {Xuezhi Wang, Jason Wei, Dale Schuurmans, Quoc V. Le, Ed H. Chi, Sharan Narang, Aakanksha Chowdhery, and Denny Zhou. Self-consistency improves chain of thought reasoning in language models. In The Eleventh International Conference on Learning Representations, ICLR 2023, Kigali, Rwanda, May 1-5, 2023. OpenReview.net, 2023b. URL https://openreview.net/ pdf?id=1PL1NIMMrw.}, } @misc{arxiv-2604.00554v1.r36, author = {Wang, Z. and Liu, J.C.}, title = {{Translating mathematical formula images to latex sequences using deep neural networks with sequence-level training}}, year = {2019}, url = {https://arxiv.org/abs/1908.11415}, note = {Z. Wang and J.C. Liu. 2019. Translating mathematical formula images to latex sequences using deep neural networks with sequence-level training. arXiv preprint (2019). arXiv:1908.11415}, } @misc{arxiv-2604.00554v1.r37, author = {Wang, Z. and Liu, J.C.}, title = {{Pdf2latex: A deep learning system to convert mathematical documents from pdf to latex}}, year = {2020}, note = {Z. Wang and J.C. Liu. 2020. Pdf2latex: A deep learning system to convert mathe- matical documents from pdf to latex. In Proceedings of the ACM Symposium on Document Engineering 2020. 1–10.}, } @article{arxiv-2512.09874v3.r39, author = {Wang, Z. and Liu, J.C.}, title = {{Translating math formula images to LaTeX sequences using deep neural networks with sequence-level training}}, year = {2021}, note = {Wang, Z., Liu, J.C.: Translating math formula images to LaTeX sequences us- ing deep neural networks with sequence-level training. International Journal on Document Analysis and Recognition (IJDAR) 24(1), 63–75 (2021)}, } @article{arxiv-2604.00554v1.r38, author = {Wang, Z. and Liu, J.C.}, title = {{Translating math formula images to LaTeX sequences using deep neural networks with sequence-level training}}, year = {2021}, note = {Z. Wang and J.C. Liu. 2021. Translating math formula images to LaTeX sequences using deep neural networks with sequence-level training. International Journal on Document Analysis and Recognition (IJDAR) 24, 1 (2021), 63–75.}, } @misc{arxiv-2406.01940v2.r60, author = {Wang, Zihan and Li, Yunxuan and Wu, Yuexin and Luo, Liangchen and Hou, Le and Yu, Hongkun and Shang, Jingbo}, title = {{Multi-step problem solving through a verifier: An empirical analysis on model-induced process supervision}}, year = {2024}, doi = {10.48550/arXiv.2402.02658}, url = {https://doi.org/10.48550/arXiv.2402.02658}, note = {Zihan Wang, Yunxuan Li, Yuexin Wu, Liangchen Luo, Le Hou, Hongkun Yu, and Jingbo Shang. Multi-step problem solving through a verifier: An empirical analysis on model-induced process supervision. CoRR, abs/2402.02658, 2024. doi: 10.48550/ARXIV.2402.02658. URL https: //doi.org/10.48550/arXiv.2402.02658.}, } @misc{arxiv-2512.09874v3.r40, author = {Wei, H. and Kong, L. and Chen, J. and Zhao, L. and Sun, Z. and Zhang, J. and Peng, C. and Shen, Y. and Mao, X. and Xu, Z.}, title = {{General ocr theory: Towards ocr-2.0 via a unified end-to-end model}}, year = {2024}, note = {Wei, H., Kong, L., Chen, J., Zhao, L., Sun, Z., Zhang, J., Peng, C., Shen, Y., Mao, X., Xu, Z., et al.: General ocr theory: Towards ocr-2.0 via a unified end-to-end model. arXiv preprint (2024)}, } @misc{arxiv-2604.00554v1.r39, author = {Wei, H. and Liu, C. and Chen, J. and Wang, J. and Kong, L. and Xu, Y. and Zhang, X.}, title = {{General OCR Theory: Towards OCR-2.0 via a Unified End-to-end Model}}, year = {2024}, url = {https://arxiv.org/abs/2409.01704}, note = {H. Wei, C. Liu, J. Chen, J. Wang, L. Kong, Y. Xu, and X. Zhang. 2024. General OCR Theory: Towards OCR-2.0 via a Unified End-to-end Model. arXiv preprint (2024). arXiv:2409.01704}, } @misc{arxiv-2512.09874v3.r41, author = {Wei, H. and Sun, Y. and Li, Y.}, title = {{Deepseek-ocr: Contexts optical compression}}, year = {2025}, note = {Wei, H., Sun, Y., Li, Y.: Deepseek-ocr: Contexts optical compression. arXiv preprint (2025)}, } @misc{arxiv-2406.01940v2.r61, author = {Wei, Jason and Wang, Xuezhi and Schuurmans, Dale and Bosma, Maarten and Ichter, Brian and Xia, Fei and Chi, Ed H. and Le, Quoc V. and Zhou, Denny}, title = {{Chain-of-thought prompting elicits reasoning in large language models}}, year = {2022}, url = {http://papers.nips.cc/paper_files/paper/2022/hash/9d5609613524ecf4f15af0f7b31abca4-Abstract-Conference.html}, note = {Jason Wei, Xuezhi Wang, Dale Schuurmans, Maarten Bosma, Brian Ichter, Fei Xia, Ed H. Chi, Quoc V. Le, and Denny Zhou. Chain-of-thought prompting elicits reasoning in large language models. In Sanmi Koyejo, S. Mohamed, A. Agarwal, Danielle Belgrave, K. Cho, and A. Oh (eds.), Advances in Neural Information Processing Systems 35: Annual Conference on Neural Information Processing Systems 2022, NeurIPS 2022, New Orleans, LA, USA, November 28 - December 9, 2022, 2022. URL http://papers.nips.cc/paper_files/paper/2022/hash/ 9d5609613524ecf4f15af0f7b31abca4-Abstract-Conference.html.}, } @misc{arxiv-2406.01940v2.r62, author = {Welleck, Sean and Lu, Ximing and West, Peter and Brahman, Faeze and Shen, Tianxiao and Khashabi, Daniel and Choi, Yejin}, title = {{Generating sequences by learning to self-correct}}, year = {2023}, url = {https://openreview.net/pdf?id=hH36JeQZDaO}, note = {Sean Welleck, Ximing Lu, Peter West, Faeze Brahman, Tianxiao Shen, Daniel Khashabi, and Yejin Choi. Generating sequences by learning to self-correct. In The Eleventh International Conference on Learning Representations, ICLR 2023, Kigali, Rwanda, May 1-5, 2023. OpenReview.net, 2023. URL https://openreview.net/pdf?id=hH36JeQZDaO.}, } @misc{arxiv-2602.16554v1.r19, author = {Weng, Ke and Du, Lun and Li, Sirui and Lu, Wangyue and Sun, Haozhe and Liu, Hengyu and Zhang, Tiancheng}, title = {{Autoformalization in the Era of Large Language Models: A Survey}}, year = {2025}, url = {http://arxiv.org/abs/2505.23486}, note = {Ke Weng, Lun Du, Sirui Li, Wangyue Lu, Haozhe Sun, Hengyu Liu, and Tiancheng Zhang. Aut- oformalization in the Era of Large Language Models: A Survey, May 2025. URL http: //arxiv.org/abs/2505.23486. arXiv:2505.23486 [cs].}, } @misc{arxiv-2406.01940v2.r63, author = {Wenzel, Makarius and Paulson, Lawrence C. and Nipkow, Tobias}, title = {{The isabelle framework}}, year = {2008}, doi = {10.1007/978-3-540-71067-7_7}, url = {https://doi.org/10.1007/978-3-540-71067-7_7}, note = {Makarius Wenzel, Lawrence C. Paulson, and Tobias Nipkow. The isabelle framework. In Otmane Aït Mohamed, C{\'{e}}sar A. Muñoz, and Sofi{\`{e}}ne Tahar (eds.), Theorem Proving in Higher Order Logics, 21st International Conference, TPHOLs 2008, Montreal, Canada, August 18-21, 2008. Proceed- ings, volume 5170 of Lecture Notes in Computer Science, pp. 33–38. Springer, 2008. doi: 10.1007/ 978-3-540-71067-7\_7. URL https://doi.org/10.1007/978-3-540-71067-7_7.}, } @misc{arxiv-2602.16554v1.r20, author = {Williamson, Dominic J. and Yoder, Theodore J.}, title = {{Low-overhead fault-tolerant quantum computation by gauging logical operators}}, year = {2024}, url = {https://arxiv.org/abs/2410.02213}, note = {Dominic J. Williamson and Theodore J. Yoder. Low-overhead fault-tolerant quantum computation by gauging logical operators, 2024. URL https://arxiv.org/abs/2410.02213.}, } @misc{arxiv-2406.01940v2.r64, author = {Wu, Jeff and Ouyang, Long and Ziegler, Daniel M. and Stiennon, Nisan and Lowe, Ryan and Leike, Jan and Christiano, Paul}, title = {{Recursively summarizing books with human feedback}}, year = {2021}, url = {https://arxiv.org/abs/2109.10862}, note = {Jeff Wu, Long Ouyang, Daniel M. Ziegler, Nisan Stiennon, Ryan Lowe, Jan Leike, and Paul Christiano. Recursively summarizing books with human feedback, 2021. URL https:// arxiv.org/abs/2109.10862.}, } @misc{arxiv-2406.01940v2.r65, author = {Wu, Yuhuai and Albert Qiaochu Jiang and Li, Wenda and Rabe, Markus N. and Staats, Charles and Jamnik, Mateja and Szegedy, Christian}, title = {{Autoformalization with large language models}}, year = {2022}, url = {http://papers.nips.cc/paper_files/paper/2022/hash/d0c6bc641a56bebee9d985b937307367-Abstract-Conference.html}, note = {Yuhuai Wu, Albert Qiaochu Jiang, Wenda Li, Markus N. Rabe, Charles Staats, Mateja Jam- nik, and Christian Szegedy. Autoformalization with large language models. In Sanmi Koyejo, S. Mohamed, A. Agarwal, Danielle Belgrave, K. Cho, and A. Oh (eds.), Advances in Neural Information Processing Systems 35: Annual Conference on Neural Information Processing Systems 2022, NeurIPS 2022, New Orleans, LA, USA, November 28 - December 9, 2022, 2022. URL http://papers.nips.cc/paper_files/paper/2022/hash/ d0c6bc641a56bebee9d985b937307367-Abstract-Conference.html.}, } @misc{arxiv-2602.16554v1.r21, author = {Wu, Yuhuai and Jiang, Albert Q. and Li, Wenda and Rabe, Markus N. and Staats, Charles and Jamnik, Mateja and Szegedy, Christian}, title = {{Autoformalization with Large Language Models}}, year = {2022}, url = {http://arxiv.org/abs/2205.12615}, note = {Yuhuai Wu, Albert Q. Jiang, Wenda Li, Markus N. Rabe, Charles Staats, Mateja Jamnik, and Christian Szegedy. Autoformalization with Large Language Models, May 2022. URL http: //arxiv.org/abs/2205.12615. arXiv:2205.12615 [cs].}, } @misc{arxiv-2406.01940v2.r66, author = {Wu, Zeqiu and Hu, Yushi and Shi, Weijia and Dziri, Nouha and Suhr, Alane and Ammanabrolu, Prithviraj and Smith, Noah A. and Ostendorf, Mari and Hajishirzi, Hannaneh}, title = {{Fine-grained human feedback gives better rewards for language model training}}, year = {2023}, url = {http://papers.nips.cc/paper_files/paper/2023/hash/b8c90b65739ae8417e61eadb521f63d5-Abstract-Conference.html}, note = {Zeqiu Wu, Yushi Hu, Weijia Shi, Nouha Dziri, Alane Suhr, Prithviraj Ammanabrolu, Noah A. Smith, Mari Ostendorf, and Hannaneh Hajishirzi. Fine-grained human feed- back gives better rewards for language model training. In Alice Oh, Tristan Naumann, Amir Globerson, Kate Saenko, Moritz Hardt, and Sergey Levine (eds.), Advances in Neural Information Processing Systems 36: Annual Conference on Neural Information Processing Systems 2023, NeurIPS 2023, New Orleans, LA, USA, December 10 - 16, 2023, 2023. URL http://papers.nips.cc/paper_files/paper/2023/hash/ b8c90b65739ae8417e61eadb521f63d5-Abstract-Conference.html.}, } @misc{arxiv-2512.09874v3.r42, author = {Xie, Y. and Mouch{\`{e}}re, H. and Simistira Liwicki, F. and Rakesh, S. and Saini, R. and Nakagawa, M. and Nguyen, C.T. and Truong, T.N.}, title = {{ICDAR 2023 CROHME: Competition on recognition of handwritten mathematical expressions}}, year = {2023}, note = {Xie, Y., Mouch{\`{e}}re, H., Simistira Liwicki, F., Rakesh, S., Saini, R., Nakagawa, M., Nguyen, C.T., Truong, T.N.: ICDAR 2023 CROHME: Competition on recognition of handwritten mathematical expressions. In: Proceedings of the 17th International Conference on Document Analysis and Recognition (ICDAR). pp. 553–565 (2023)}, } @misc{arxiv-2601.22554v1.r23, author = {Xin, Huajian and Ren, Z. Z. and Song, Junxiao and Shao, Zhihong and Zhao, Wanjia and Wang, Haocheng and Liu, Bo and Zhang, Liyue and Lu, Xuan and Du, Qiushi}, title = {{DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search}}, year = {2024}, doi = {10.48550/arXiv.2408.08152}, url = {https://doi.org/10.48550/arXiv.2408.08152}, note = {Huajian Xin, Z. Z. Ren, Junxiao Song, Zhihong Shao, Wanjia Zhao, Haocheng Wang, Bo Liu, Liyue Zhang, Xuan Lu, Qiushi Du, et al. DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search. arXiv preprint, 2024. doi: 10.48550/arXiv.2408.08152. URL https://doi.org/10.48550/arXiv.2408.08152.}, } @misc{arxiv-2601.22554v1.r22, author = {Xin, Huajian and Guo, Daya and Shao, Zhihong and Ren, Zhizhou and Zhu, Qihao and Liu, Bo and Ruan, Chong and Li, Wenda and Liang, Xiaodan}, title = {{DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data}}, year = {2024}, doi = {10.48550/arXiv.2405.14333}, url = {https://arxiv.org/abs/2405.14333}, note = {Huajian Xin, Daya Guo, Zhihong Shao, Zhizhou Ren, Qihao Zhu, Bo Liu, Chong Ruan, Wenda Li, and Xiaodan Liang. DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data. arXiv preprint, 2024. doi: 10.48550/arXiv.2405.14333. URL https://doi.org/10.48550/arXiv .2405.14333.}, } @misc{arxiv-2602.16554v1.r22, author = {Xin, Huajian and Guo, Daya and Shao, Zhihong and Ren, Zhizhou and Zhu, Qihao and Liu, Bo and Ruan, Chong and Li, Wenda and Liang, Xiaodan}, title = {{Deepseek-prover: Advancing theorem proving in llms through large-scale synthetic data}}, year = {2024}, url = {https://arxiv.org/abs/2405.14333}, note = {Huajian Xin, Daya Guo, Zhihong Shao, Zhizhou Ren, Qihao Zhu, Bo Liu, Chong Ruan, Wenda Li, and Xiaodan Liang. Deepseek-prover: Advancing theorem proving in llms through large-scale synthetic data, 2024. URL https://arxiv.org/abs/2405.14333.}, } @misc{arxiv-2406.01940v2.r67, author = {Xiong, Jing and Li, Zixuan and Zheng, Chuanyang and Guo, Zhijiang and Yin, Yichun and Xie, Enze and Yang, Zhicheng and Cao, Qingxing and Wang, Haiming and Han, Xiongwei}, title = {{Dq-lore: Dual queries with low rank approximation re-ranking for in-context learning}}, year = {2023}, url = {https://arxiv.org/abs/2310.02954}, note = {Jing Xiong, Zixuan Li, Chuanyang Zheng, Zhijiang Guo, Yichun Yin, Enze Xie, Zhicheng Yang, Qingxing Cao, Haiming Wang, Xiongwei Han, et al. Dq-lore: Dual queries with low rank approximation re-ranking for in-context learning. arXiv preprint arXiv:2310.02954, 2023a.}, } @misc{arxiv-2406.01940v2.r68, author = {Xiong, Jing and Shen, Jianhao and Yuan, Ye and Wang, Haiming and Yin, Yichun and Liu, Zhengying and Li, Lin and Guo, Zhijiang and Cao, Qingxing and Huang, Yinya and Zheng, Chuanyang and Liang, Xiaodan and Zhang, Ming and Liu, Qun}, title = {{TRIGO: benchmarking formal mathematical proof reduction for generative language models}}, year = {2023}, doi = {10.18653/v1/2023.emnlp-main.711}, url = {https://doi.org/10.18653/v1/2023.emnlp-main.711}, note = {Jing Xiong, Jianhao Shen, Ye Yuan, Haiming Wang, Yichun Yin, Zhengying Liu, Lin Li, Zhi- jiang Guo, Qingxing Cao, Yinya Huang, Chuanyang Zheng, Xiaodan Liang, Ming Zhang, and Qun Liu. TRIGO: benchmarking formal mathematical proof reduction for generative language models. In Houda Bouamor, Juan Pino, and Kalika Bali (eds.), Proceedings of the 2023 Con- ference on Empirical Methods in Natural Language Processing, EMNLP 2023, Singapore, De- cember 6-10, 2023, pp. 11594–11632. Association for Computational Linguistics, 2023b. doi: 10.18653/V1/2023.EMNLP-MAIN.711. URL https://doi.org/10.18653/v1/2023. emnlp-main.711.}, } @misc{arxiv-2602.16554v1.r23, author = {Xu, Yichen and Odersky, Martin}, title = {{Agentic Proof Automation: A Case Study}}, year = {2026}, url = {http://arxiv.org/abs/2601.03768}, note = {Yichen Xu and Martin Odersky. Agentic Proof Automation: A Case Study, January 2026. URL http://arxiv.org/abs/2601.03768. arXiv:2601.03768 [cs].}, } @misc{arxiv-2406.01940v2.r69, author = {Yang, Kaiyu and Deng, Jia}, title = {{Learning to prove theorems via interacting with proof assistants}}, year = {2019}, url = {http://proceedings.mlr.press/v97/yang19a.html}, note = {Kaiyu Yang and Jia Deng. Learning to prove theorems via interacting with proof assistants. In Kamalika Chaudhuri and Ruslan Salakhutdinov (eds.), Proceedings of the 36th International Conference on Machine Learning, ICML 2019, 9-15 June 2019, Long Beach, California, USA, volume 97 of Proceedings of Machine Learning Research, pp. 6984–6994. PMLR, 2019. URL http://proceedings.mlr.press/v97/yang19a.html.}, } @misc{arxiv-2406.01940v2.r70, author = {Yang, Kaiyu and Swope, Aidan M. and Gu, Alex and Chalamala, Rahul and Song, Peiyang and Yu, Shixing and Godil, Saad and Prenger, Ryan J. and Anandkumar, Animashree}, year = {2023}, url = {http://papers.nips.cc/paper_files/paper/2023/hash/4441469427094f8873d0fecb0c4e1cee-Abstract-Datasets_and_Benchmarks.html}, note = {Kaiyu Yang, Aidan M. Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan J. Prenger, and Animashree Anandkumar. Leandojo: Theorem proving with retrieval- augmented language models. In Alice Oh, Tristan Naumann, Amir Globerson, Kate Saenko, Moritz Hardt, and Sergey Levine (eds.), Advances in Neural Information Processing Systems 36: Annual Conference on Neural Information Processing Systems 2023, NeurIPS 2023, New Orleans, LA, USA, December 10 - 16, 2023, 2023a. URL http://papers.nips.cc/paper_files/paper/ 2023/hash/4441469427094f8873d0fecb0c4e1cee-Abstract-Datasets_ and_Benchmarks.html.}, } @misc{arxiv-2406.01940v2.r71, author = {Yang, Kaiyu and Swope, Aidan M. and Gu, Alex and Chalamala, Rahul and Song, Peiyang and Yu, Shixing and Godil, Saad and Prenger, Ryan J. and Anandkumar, Animashree}, year = {2023}, url = {http://papers.nips.cc/paper_files/paper/2023/hash/4441469427094f8873d0fecb0c4e1cee-Abstract-Datasets_and_Benchmarks.html}, note = {Kaiyu Yang, Aidan M. Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan J. Prenger, and Animashree Anandkumar. Leandojo: Theorem proving with retrieval- augmented language models. In Alice Oh, Tristan Naumann, Amir Globerson, Kate Saenko, Moritz Hardt, and Sergey Levine (eds.), Advances in Neural Information Processing Systems 36: Annual Conference on Neural Information Processing Systems 2023, NeurIPS 2023, New Orleans, LA, USA, December 10 - 16, 2023, 2023b. URL http://papers.nips.cc/paper_files/paper/ 2023/hash/4441469427094f8873d0fecb0c4e1cee-Abstract-Datasets_ and_Benchmarks.html.}, } @misc{arxiv-2601.22554v1.r24, author = {Yang, Kaiyu and Swope, Aidan and Gu, Alex and Chalamala, Rahul and Song, Peiyang and Yu, Shixing and Godil, Saad and Prenger, Ryan J. and Anandkumar, Animashree}, title = {{LeanDojo: Theorem Proving with Retrieval-Augmented Language Models}}, year = {2023}, note = {Kaiyu Yang, Aidan Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan J. Prenger, and Animashree Anandkumar. LeanDojo: Theorem Proving with Retrieval-Augmented Language Models. Advances in Neural Information Processing Systems, 36:21573–21612, 2023.}, } @misc{arxiv-2406.01940v2.r72, author = {Yao, Yuxuan and Wu, Han and Guo, Zhijiang and Zhou, Biyan and Gao, Jiahui and Luo, Sichun and Hou, Hanxu and Fu, Xiaojin and Song, Linqi}, title = {{Learning from correctness without prompting makes llm efficient reasoner}}, year = {2024}, url = {https://arxiv.org/abs/2403.19094}, note = {Yuxuan Yao, Han Wu, Zhijiang Guo, Biyan Zhou, Jiahui Gao, Sichun Luo, Hanxu Hou, Xiaojin Fu, and Linqi Song. Learning from correctness without prompting makes llm efficient reasoner. arXiv preprint arXiv:2403.19094, 2024.}, } @misc{arxiv-2406.01940v2.r73, author = {Yasunaga, Michihiro and Chen, Xinyun and Li, Yujia and Pasupat, Panupong and Leskovec, Jure and Liang, Percy and Chi, Ed H. and Zhou, Denny}, title = {{Large language models as analogical reasoners}}, year = {2023}, doi = {10.48550/arXiv.2310.01714}, url = {https://doi.org/10.48550/arXiv.2310.01714}, note = {Michihiro Yasunaga, Xinyun Chen, Yujia Li, Panupong Pasupat, Jure Leskovec, Percy Liang, Ed H. Chi, and Denny Zhou. Large language models as analogical reasoners. CoRR, abs/2310.01714, 2023. doi: 10.48550/ARXIV.2310.01714. URL https://doi.org/10.48550/arXiv. 2310.01714.}, } @misc{arxiv-2406.01940v2.r74, author = {Ye, Xi and Durrett, Greg}, title = {{The unreliability of explanations in few-shot prompting for textual reasoning}}, year = {2022}, url = {http://papers.nips.cc/paper_files/paper/2022/hash/c402501846f9fe03e2cac015b3f0e6b1-Abstract-Conference.html}, note = {Xi Ye and Greg Durrett. The unreliability of explanations in few-shot prompting for textual reasoning. In Sanmi Koyejo, S. Mohamed, A. Agarwal, Danielle Belgrave, K. Cho, and A. Oh (eds.), Advances in Neural Information Processing Systems 35: Annual Conference on Neural Information Processing Systems 2022, NeurIPS 2022, New Orleans, LA, USA, November 28 - December 9, 2022, 2022. URL http://papers.nips.cc/paper_files/paper/2022/hash/ c402501846f9fe03e2cac015b3f0e6b1-Abstract-Conference.html.}, } @misc{arxiv-2406.01940v2.r76, author = {Ying, Huaiyuan and Zhang, Shuo and Li, Linyang and Zhou, Zhejian and Shao, Yunfan and Fei, Zhaoye and Ma, Yichuan and Hong, Jiawei and Liu, Kuikun and Wang, Ziyi and Wang, Yudong and Wu, Zijian and Li, Shuaibin and Zhou, Fengzhe and Liu, Hongwei and Zhang, Songyang and Zhang, Wenwei and Yan, Hang and Qiu, Xipeng and Wang, Jiayu and Chen, Kai and Lin, Dahua}, title = {{Internlm-math: Open math large language models toward verifiable reasoning}}, year = {2024}, doi = {10.48550/arXiv.2402.06332}, url = {https://doi.org/10.48550/arXiv.2402.06332}, note = {Huaiyuan Ying, Shuo Zhang, Linyang Li, Zhejian Zhou, Yunfan Shao, Zhaoye Fei, Yichuan Ma, Jiawei Hong, Kuikun Liu, Ziyi Wang, Yudong Wang, Zijian Wu, Shuaibin Li, Fengzhe Zhou, Hongwei Liu, Songyang Zhang, Wenwei Zhang, Hang Yan, Xipeng Qiu, Jiayu Wang, Kai Chen, and Dahua Lin. Internlm-math: Open math large language models toward verifiable reasoning. CoRR, abs/2402.06332, 2024b. doi: 10.48550/ARXIV.2402.06332. URL https://doi.org/ 10.48550/arXiv.2402.06332.}, } @misc{arxiv-2406.01940v2.r77, author = {Ying, Huaiyuan and Zhang, Shuo and Li, Linyang and Zhou, Zhejian and Shao, Yunfan and Fei, Zhaoye and Ma, Yichuan and Hong, Jiawei and Liu, Kuikun and Wang, Ziyi and Wang, Yudong and Wu, Zijian and Li, Shuaibin and Zhou, Fengzhe and Liu, Hongwei and Zhang, Songyang and Zhang, Wenwei and Yan, Hang and Qiu, Xipeng and Wang, Jiayu and Chen, Kai and Lin, Dahua}, title = {{Internlm-math: Open math large language models toward verifiable reasoning}}, year = {2024}, doi = {10.48550/arXiv.2402.06332}, url = {https://doi.org/10.48550/arXiv.2402.06332}, note = {Huaiyuan Ying, Shuo Zhang, Linyang Li, Zhejian Zhou, Yunfan Shao, Zhaoye Fei, Yichuan Ma, Jiawei Hong, Kuikun Liu, Ziyi Wang, Yudong Wang, Zijian Wu, Shuaibin Li, Fengzhe Zhou, Hongwei Liu, Songyang Zhang, Wenwei Zhang, Hang Yan, Xipeng Qiu, Jiayu Wang, Kai Chen, and Dahua Lin. Internlm-math: Open math large language models toward verifiable reasoning. CoRR, abs/2402.06332, 2024c. doi: 10.48550/ARXIV.2402.06332. URL https://doi.org/ 10.48550/arXiv.2402.06332.}, } @misc{arxiv-2406.01940v2.r75, author = {Ying, Huaiyuan and Wu, Zijian and Geng, Yihan and Wang, Jiayu and Lin, Dahua and Chen, Kai}, title = {{Lean workbook: A large-scale lean problem set formalized from natural language math problems}}, year = {2024}, doi = {10.48550/arXiv.2406.03847}, url = {https://doi.org/10.48550/arXiv.2406.03847}, note = {Huaiyuan Ying, Zijian Wu, Yihan Geng, Jiayu Wang, Dahua Lin, and Kai Chen. Lean work- book: A large-scale lean problem set formalized from natural language math problems. CoRR, abs/2406.03847, 2024a. doi: 10.48550/ARXIV.2406.03847. URL https://doi.org/10. 48550/arXiv.2406.03847.}, } @misc{arxiv-2406.01940v2.r78, author = {Yu, Fei and Gao, Anningzhe and Wang, Benyou}, title = {{Outcome-supervised verifiers for planning in thematical reasoning}}, year = {2023}, doi = {10.48550/arXiv.2311.09724}, url = {https://doi.org/10.48550/arXiv.2311.09724}, note = {Fei Yu, Anningzhe Gao, and Benyou Wang. Outcome-supervised verifiers for planning in thematical reasoning. CoRR, abs/2311.09724, 2023a. doi: 10.48550/ARXIV.2311.09724. URL https: //doi.org/10.48550/arXiv.2311.09724.}, } @misc{arxiv-2406.01940v2.r79, author = {Yu, Wenhao and Zhang, Zhihan and Liang, Zhenwen and Jiang, Meng and Sabharwal, Ashish}, title = {{Improving language models via plug-and-play retrieval feedback}}, year = {2023}, doi = {10.48550/arXiv.2305.14002}, url = {https://doi.org/10.48550/arXiv.2305.14002}, note = {Wenhao Yu, Zhihan Zhang, Zhenwen Liang, Meng Jiang, and Ashish Sabharwal. Improving language models via plug-and-play retrieval feedback. CoRR, abs/2305.14002, 2023b. doi: 10.48550/ ARXIV.2305.14002. URL https://doi.org/10.48550/arXiv.2305.14002.}, } @misc{arxiv-2003.08005v1.r34, author = {Yu, Z. and Lyu, S. and Lu, Y. and Wang, P. S.}, title = {{A fusion strategy for the single shot text detector}}, year = {2018}, note = {Z. Yu, S. Lyu, Y. Lu, and P. S. Wang, “A fusion strategy for the single shot text detector,” in 2018 24th International Conference on Pattern Recognition (ICPR). IEEE, 2018, pp. 3687–3691.}, } @misc{arxiv-2512.09874v3.r43, author = {Yuan, Y. and Liu, X. and Dikubab, W. and Liu, H. and Ji, Z. and Wu, Z. and Bai, X.}, title = {{Syntax-aware network for handwritten mathematical expression recognition}}, year = {2022}, note = {Yuan, Y., Liu, X., Dikubab, W., Liu, H., Ji, Z., Wu, Z., Bai, X.: Syntax-aware network for handwritten mathematical expression recognition. In: Proceedings of the IEEE/CVF Conference on Computer Vision and Pattern Recognition (CVPR). pp. 4543–4552 (2022)}, } @misc{arxiv-2406.01940v2.r80, author = {Yuan, Zheng and Yuan, Hongyi and Li, Chengpeng and Dong, Guanting and Tan, Chuanqi and Zhou, Chang}, title = {{Scaling relationship on learning mathematical reasoning with large language models}}, year = {2023}, doi = {10.48550/arXiv.2308.01825}, url = {https://doi.org/10.48550/arXiv.2308.01825}, note = {Zheng Yuan, Hongyi Yuan, Chengpeng Li, Guanting Dong, Chuanqi Tan, and Chang Zhou. Scaling re- lationship on learning mathematical reasoning with large language models. CoRR, abs/2308.01825, 2023. doi: 10.48550/ARXIV.2308.01825. URL https://doi.org/10.48550/arXiv. 2308.01825.}, } @misc{arxiv-2406.01940v2.r81, author = {Zeng, Zhongshen and Liu, Yinhong and Wan, Yingjia and Li, Jingyao and Chen, Pengguang and Dai, Jianbo and Yao, Yuxuan and Xu, Rongwu and Qi, Zehan and Zhao, Wanru and Shen, Linling and Lu, Jianqiao and Tan, Haochen and Chen, Yukang and Zhang, Hao and Shi, Zhan and Wang, Bailin and Guo, Zhijiang and Jia, Jiaya}, title = {{Mr-ben: A comprehensive meta-reasoning benchmark for large language models}}, year = {2024}, url = {https://arxiv.org/abs/2406.13975}, note = {Zhongshen Zeng, Yinhong Liu, Yingjia Wan, Jingyao Li, Pengguang Chen, Jianbo Dai, Yuxuan Yao, Rongwu Xu, Zehan Qi, Wanru Zhao, Linling Shen, Jianqiao Lu, Haochen Tan, Yukang Chen, Hao Zhang, Zhan Shi, Bailin Wang, Zhijiang Guo, and Jiaya Jia. Mr-ben: A comprehensive meta-reasoning benchmark for large language models. CoRR, abs/2406.13975, 2024. URL https://arxiv.org/abs/2406.13975.}, } @misc{arxiv-2602.16554v1.r24, author = {Zhang, Hanning and Wang, Ruida and Pan, Rui and Wang, Wenyuan and Meng, Bingxu and Zhang, Tong}, title = {{PhysProver: Advancing Automatic Theorem Proving for Physics}}, year = {2026}, url = {http://arxiv.org/abs/2601.15737}, note = {Hanning Zhang, Ruida Wang, Rui Pan, Wenyuan Wang, Bingxu Meng, and Tong Zhang. PhysProver: Advancing Automatic Theorem Proving for Physics, January 2026. URL http://arxiv.org/ abs/2601.15737. arXiv:2601.15737 [cs].}, } @article{arxiv-2003.08005v1.r12, author = {Zhang, J. and Du, J. and Zhang, S. and Liu, D. and Hu, Y. and Hu, J. and Wei, S. and Dai, L.}, title = {{Watch, attend and parse: An end-to-end neural network based approach to handwritten mathematical expression recognition}}, year = {2017}, note = {J. Zhang, J. Du, S. Zhang, D. Liu, Y. Hu, J. Hu, S. Wei, and L. Dai, “Watch, attend and parse: An end-to-end neural network based approach to handwritten mathematical expression recognition,” Pattern Recognition, vol. 71, pp. 196–206, 2017.}, } @article{arxiv-2003.08005v1.r10, author = {Zhang, J. and Du, J. and Dai, L.}, title = {{Track, attend, and parse (tap): An end-to-end framework for online handwritten mathematical expression recognition}}, year = {2018}, note = {J. Zhang, J. Du, and L. Dai, “Track, attend, and parse (tap): An end-to-end framework for online handwritten mathematical expression recognition,” IEEE Transactions on Multimedia, vol. 21, no. 1, pp. 221– 233, 2018.}, } @misc{arxiv-2602.16554v1.r25, author = {Zhang, Lan and Valentino, Marco and Freitas, Andre}, title = {{Autoformalization in the Wild: Assessing LLMs on Real-World Mathematical Definitions}}, year = {2025}, url = {http://arxiv.org/abs/2502.12065}, note = {Lan Zhang, Marco Valentino, and Andre Freitas. Autoformalization in the Wild: Assessing LLMs on Real-World Mathematical Definitions, September 2025. URL http://arxiv.org/abs/ 2502.12065. arXiv:2502.12065 [cs].}, } @misc{arxiv-2512.09874v3.r44, author = {Zhang, Q. and Wang, B. and Huang, V.S.J. and Zhang, J. and Wang, Z. and Liang, H. and He, C. and Zhang, W.}, title = {{Document parsing unveiled: Techniques, challenges, and prospects for structured information extraction}}, year = {2025}, note = {Zhang, Q., Wang, B., Huang, V.S.J., Zhang, J., Wang, Z., Liang, H., He, C., Zhang, W.: Document parsing unveiled: Techniques, challenges, and prospects for structured information extraction. arXiv preprint (2025)}, } @article{arxiv-2604.00554v1.r40, author = {Zhang, X. and Zhou, Z. and Ming, C. and Sun, Y.Y.}, title = {{GPT-Assisted Learning of Structure–Property Relationships by Graph Neural Networks: Application to Rare-Earth-Doped Phosphors}}, year = {2023}, note = {X. Zhang, Z. Zhou, C. Ming, and Y.Y. Sun. 2023. GPT-Assisted Learning of Structure–Property Relationships by Graph Neural Networks: Application to Rare-Earth-Doped Phosphors. The Journal of Physical Chemistry Letters 14, 50 (2023), 11342–11349.}, } @misc{arxiv-2406.01940v2.r82, author = {Zhang, Xiaokai and Zhu, Na and He, Yiming and Zou, Jia and Huang, Qike and Jin, Xiaoxiao and Guo, Yanjun and Mao, Chenyang and Zhu, Zhe and Yue, Dengfeng and Zhu, Fangzhen and Li, Yang and Wang, Yifan and Huang, Yiwen and Wang, Runan and Qin, Cheng and Zeng, Zhen and Xie, Shaorong and Luo, Xiangfeng and Leng, Tuo}, title = {{Formalgeo: The first step toward human-like imo-level geometric automated reasoning}}, year = {2023}, url = {https://api.semanticscholar.org/CorpusID:264555630}, note = {Xiaokai Zhang, Na Zhu, Yiming He, Jia Zou, Qike Huang, Xiaoxiao Jin, Yanjun Guo, Chenyang Mao, Zhe Zhu, Dengfeng Yue, Fangzhen Zhu, Yang Li, Yifan Wang, Yiwen Huang, Runan Wang, Cheng Qin, Zhen Zeng, Shaorong Xie, Xiangfeng Luo, and Tuo Leng. Formalgeo: The first step toward human-like imo-level geometric automated reasoning. ArXiv, abs/2310.18021, 2023. URL https://api.semanticscholar.org/CorpusID:264555630.}, } @misc{arxiv-2601.22554v1.r25, author = {Zheng, Kunhao and Jesse Michael Han and Polu, Stanislas}, title = {{miniF2F: A Cross-System Benchmark for Formal Olympiad-Level Mathematics}}, year = {2021}, doi = {10.48550/arXiv.2109.00110}, url = {https://doi.org/10.48550/arXiv.2109.00110}, note = {Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. miniF2F: A Cross-System Benchmark for Formal Olympiad-Level Mathematics. arXiv preprint, 2021. doi: 10.48550/arXiv.2109.00110. URL https://doi.org/10.48550/arXiv.2109.00110.}, } @misc{arxiv-2406.01940v2.r83, author = {Zheng, Kunhao and Jesse Michael Han and Polu, Stanislas}, title = {{minif2f: a cross-system benchmark for formal olympiad-level mathematics}}, year = {2022}, url = {https://openreview.net/forum?id=9ZPegFuFTFv}, note = {Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. minif2f: a cross-system benchmark for formal olympiad-level mathematics. In The Tenth International Conference on Learning Representations, ICLR 2022, Virtual Event, April 25-29, 2022. OpenReview.net, 2022a. URL https://openreview.net/forum?id=9ZPegFuFTFv.}, } @misc{arxiv-2406.01940v2.r84, author = {Zheng, Kunhao and Jesse Michael Han and Polu, Stanislas}, title = {{minif2f: a cross-system benchmark for formal olympiad-level mathematics}}, year = {2022}, url = {https://openreview.net/forum?id=9ZPegFuFTFv}, note = {Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. minif2f: a cross-system benchmark for formal olympiad-level mathematics. In The Tenth International Conference on Learning Representations, ICLR 2022, Virtual Event, April 25-29, 2022. OpenReview.net, 2022b. URL https://openreview.net/forum?id=9ZPegFuFTFv.}, } @misc{arxiv-2604.00554v1.r41, author = {Zheng, Sixiao and Lu, Jiachen and Zhao, Hengshuang and Zhu, Xiatian and Luo, Zekun and Wang, Yabiao and Fu, Yanwei and Feng, Jianfeng and Xiang, Tao and Torr, Philip HS}, year = {2021}, note = {Sixiao Zheng, Jiachen Lu, Hengshuang Zhao, Xiatian Zhu, Zekun Luo, Yabiao Wang, Yanwei Fu, Jianfeng Feng, Tao Xiang, Philip HS Torr, et al. 2021. Re- thinking semantic segmentation from a sequence-to-sequence perspective with transformers. In Proceedings of the IEEE/CVF conference on computer vision and pattern recognition. 6881–6890.}, } @misc{arxiv-2604.00554v1.r42, author = {Zheng, Yaowei and Zhang, Richong and Zhang, Junhao and Ye, Yanhan and Luo, Zheyan and Feng, Zhangchi and Ma, Yongqiang}, title = {{LlamaFactory: Unified Efficient Fine-Tuning of 100+ Language Models}}, year = {2024}, url = {http://arxiv.org/abs/2403.13372}, note = {Yaowei Zheng, Richong Zhang, Junhao Zhang, Yanhan Ye, Zheyan Luo, Zhangchi Feng, and Yongqiang Ma. 2024. LlamaFactory: Unified Efficient Fine-Tuning of 100+ Language Models. In Proceedings of the 62nd Annual Meeting of the Association for Computational Linguistics (Volume 3: System Demonstrations). Association for Computational Linguistics, Bangkok, Thailand. http://arxiv.org/ abs/2403.13372}, } @misc{arxiv-2512.09874v3.r46, author = {Zhong, X. and Tang, J. and Yepes, A.J.}, title = {{Publaynet: Largest dataset ever for document layout analysis}}, year = {2019}, note = {Zhong, X., Tang, J., Yepes, A.J.: Publaynet: Largest dataset ever for document lay- out analysis. In: Proceedings of the International Conference on Document Analysis and Recognition (ICDAR). pp. 1015–1022 (2019)}, } @misc{arxiv-2512.09874v3.r45, author = {Zhong, X. and ShafieiBavani, E. and Jimeno Yepes, A.}, title = {{Image-based table recognition: Data, model, and evaluation}}, year = {2020}, note = {Zhong, X., ShafieiBavani, E., Jimeno Yepes, A.: Image-based table recognition: Data, model, and evaluation. In: Proceedings of the European Conference on Com- puter Vision (ECCV). pp. 564–580 (2020)}, } @misc{arxiv-2604.00554v1.r43, author = {Zhong, Xu and Tang, Jianbin and Antonio Jimeno Yepes}, title = {{Publaynet: largest dataset ever for document layout analysis}}, year = {2019}, note = {Xu Zhong, Jianbin Tang, and Antonio Jimeno Yepes. 2019. Publaynet: largest dataset ever for document layout analysis. In 2019 International conference on document analysis and recognition (ICDAR). IEEE, 1015–1022.}, } @misc{arxiv-2406.01940v2.r85, author = {Zhou, Yongchao and Andrei Ioan Muresanu and Han, Ziwen and Paster, Keiran and Pitis, Silviu and Chan, Harris and Ba, Jimmy}, title = {{Large language models are human-level prompt engineers}}, year = {2023}, url = {https://openreview.net/pdf?id=92gvk82DE-}, note = {Yongchao Zhou, Andrei Ioan Muresanu, Ziwen Han, Keiran Paster, Silviu Pitis, Harris Chan, and Jimmy Ba. Large language models are human-level prompt engineers. In The Eleventh International Conference on Learning Representations, ICLR 2023, Kigali, Rwanda, May 1-5, 2023. OpenReview.net, 2023. URL https://openreview.net/pdf?id=92gvk82DE-.}, } @misc{arxiv-2601.22554v1.r26, author = {Zhu, Thomas and Clune, Joshua and Avigad, Jeremy and Albert Qiaochu Jiang and Welleck, Sean}, title = {{Premise Selection for a Lean Hammer}}, year = {2025}, doi = {10.48550/arXiv.2506.07477}, url = {https://arxiv.org/abs/2506.07477}, note = {Thomas Zhu, Joshua Clune, Jeremy Avigad, Albert Qiaochu Jiang, and Sean Welleck. Premise Selection for a Lean Hammer. arXiv preprint, 2025. doi: 10.48550/arXiv.2506.07477. URL https://doi.org/10 .48550/arXiv.2506.07477.}, } @misc{arxiv-2604.00554v1.r44, author = {Zhu, Wenzhen and Sokhandan, Negin and Yang, Guang and Martin, Sujitha and Sathyanarayana, Suchitra}, title = {{DocBed: A multi-stage OCR solution for documents with complex layouts}}, year = {2022}, note = {Wenzhen Zhu, Negin Sokhandan, Guang Yang, Sujitha Martin, and Suchitra Sathyanarayana. 2022. DocBed: A multi-stage OCR solution for documents with complex layouts. In Proceedings of the AAAI Conference on Artificial Intelligence, Vol. 36. 12643–12649.}, }