INT: An Inequality Benchmark for Evaluating Generalization in Theorem Proving. - Yuhuai Wu; Albert Q. Jiang; Jimmy Ba; Roger Baker Grosse (ICLR, 2021)

Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers. - Albert Qiaochu Jiang; Wenda Li; Szymon Tworkowski; Konrad Czechowski; Tomasz Odrzygózdz; Piotr Milos; Yuhuai Wu; Mateja Jamnik (NeurIPS, 2022)

Autoformalization with Large Language Models. - Yuhuai Wu; Albert Qiaochu Jiang; Wenda Li; Markus N. Rabe; Charles Staats; Mateja Jamnik; Christian Szegedy (NeurIPS, 2022)

Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs. - Albert Qiaochu Jiang; Sean Welleck; Jin Peng Zhou; Timothée Lacroix; Jiacheng Liu 010; Wenda Li; Mateja Jamnik; Guillaume Lample; Yuhuai Wu (ICLR, 2023)

Magnushammer: A Transformer-based Approach to Premise Selection. - Maciej Mikula; Szymon Antoniak; Szymon Tworkowski; Albert Qiaochu Jiang; Jin Peng Zhou; Christian Szegedy; Lukasz Kucinski; Piotr Milos; Yuhuai Wu (CoRR, 2023)

Evaluating Language Models for Mathematics through Interactions. - Katherine M. Collins; Albert Q. Jiang; Simon Frieder; Lionel Wong; Miri Zilka; Umang Bhatt; Thomas Lukasiewicz; Yuhuai Wu; Joshua B. Tenenbaum; William Hart; Timothy Gowers; Wenda Li; et al. (CoRR, 2023)

Mistral 7B. - Albert Q. Jiang; Alexandre Sablayrolles; Arthur Mensch; Chris Bamford 001; Devendra Singh Chaplot; Diego de Las Casas; Florian Bressand; Gianna Lengyel; Guillaume Lample; Lucile Saulnier; Lélio Renard Lavaud; Marie-Anne Lachaux; et al. (CoRR, 2023)

Multilingual Mathematical Autoformalization. - Albert Q. Jiang; Wenda Li; Mateja Jamnik (CoRR, 2023)

Llemma: An Open Language Model for Mathematics. - Zhangir Azerbayev; Hailey Schoelkopf; Keiran Paster; Marco Dos Santos; Stephen Marcus McAleer; Albert Q. Jiang; Jia Deng; Stella Biderman; Sean Welleck (ICLR, 2024)

Magnushammer: A Transformer-Based Approach to Premise Selection. - Maciej Mikula; Szymon Tworkowski; Szymon Antoniak; Bartosz Piotrowski; Albert Q. Jiang; Jin Peng Zhou; Christian Szegedy; Lukasz Kucinski; Piotr Milos; Yuhuai Wu (ICLR, 2024)

Multi-language Diversity Benefits Autoformalization. - Albert Q. Jiang; Wenda Li; Mateja Jamnik (NeurIPS, 2024)

Repurposing Language Models into Embedding Models: Finding the Compute-Optimal Recipe. - Albert Q. Jiang; Alicja Ziarko; Bartosz Piotrowski; Wenda Li; Mateja Jamnik; Piotr Milos (NeurIPS, 2024)

End-to-End Ontology Learning with Large Language Models. - Andy Lo; Albert Q. Jiang; Wenda Li; Mateja Jamnik (NeurIPS, 2024)

Mixtral of Experts. - Albert Q. Jiang; Alexandre Sablayrolles; Antoine Roux; Arthur Mensch; Blanche Savary; Chris Bamford 001; Devendra Singh Chaplot; Diego de Las Casas; Emma Bou Hanna; Florian Bressand; Gianna Lengyel; Guillaume Bour; et al. (CoRR, 2024)

Pixtral 12B. - Pravesh Agrawal; Szymon Antoniak; Emma Bou Hanna; Baptiste Bout; Devendra Singh Chaplot; Jessica Chudnovsky; Diogo Costa; Baudouin De Monicault; Saurabh Garg; Théophile Gervet; Soham Ghosh; Amélie Héliou; et al. (CoRR, 2024)

Premise Selection for a Lean Hammer. - Thomas Zhu; Joshua Clune; Jeremy Avigad; Albert Qiaochu Jiang; Sean Welleck (CoRR, 2025)

Magistral. - Abhinav Rastogi; Albert Q. Jiang; Andy Lo; Gabrielle Berrada; Guillaume Lample; Jason Rute; Joep Barmentlo; Karmesh Yadav; Kartik Khandelwal; Khyathi Raghavi Chandu; Léonard Blier; Lucile Saulnier; et al. (CoRR, 2025)

Voxtral. - Alexander H. Liu; Andy Ehrenberg; Andy Lo; Clément Denoix; Corentin Barreau; Guillaume Lample; Jean-Malo Delignon; Khyathi Raghavi Chandu; Patrick von Platen; Pavankumar Reddy Muddireddy; Sanchit Gandhi; Soham Ghosh; et al. (CoRR, 2025)