| Mistral 7B AQ Jiang, A Sablayrolles, A Mensch, C Bamford, DS Chaplot, ... | 7587* | 2023 |
| Mixtral of experts AQ Jiang, A Sablayrolles, A Roux, A Mensch, B Savary, C Bamford, ... arXiv preprint arXiv:2401.04088, 2024 | 3213* | 2024 |
| Llemma: An open language model for mathematics Z Azerbayev, H Schoelkopf, K Paster, MD Santos, S McAleer, AQ Jiang, ... arXiv preprint arXiv:2310.10631, 2023 | 491 | 2023 |
| Autoformalization with large language models Y Wu, AQ Jiang, W Li, MN Rabe, C Staats, M Jamnik, C Szegedy NeurIPS 2022, 2022 | 333 | 2022 |
| Draft, sketch, and prove: Guiding formal theorem provers with informal proofs AQ Jiang*, S Welleck*, JP Zhou*, W Li, J Liu, M Jamnik, T Lacroix, Y Wu, ... arXiv preprint arXiv:2210.12283, 2022 | 292 | 2022 |
| Pixtral 12B P Agrawal, S Antoniak, EB Hanna, B Bout, D Chaplot, J Chudnovsky, ... arXiv preprint arXiv:2410.07073, 2024 | 257* | 2024 |
| Numinamath: The largest public dataset in ai4maths with 860k pairs of competition math problems and solutions J Li, E Beeching, L Tunstall, B Lipkin, R Soletskyi, S Huang, K Rasul, L Yu, ... Hugging Face repository 13 (9), 9, 2024 | 203 | 2024 |
| Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers AQ Jiang, W Li, S Tworkowski, K Czechowski, T Odrzygóźdź, P Miłoś, ... NeurIPS 2022, 2022 | 158 | 2022 |
| Evaluating language models for mathematics through interactions KM Collins*, AQ Jiang*, S Frieder, L Wong, M Zilka, U Bhatt, ... Proceedings of the National Academy of Sciences 121 (24), e2318124121, 2024 | 124 | 2024 |
| LISA: Language models of isabelle proofs AQ Jiang, W Li, JM Han, Y Wu 6th Conference on Artificial Intelligence and Theorem Proving, 2021 | 108 | 2021 |
| INT: An Inequality Benchmark for Evaluating Generalization in Theorem Proving Y Wu*, AQ Jiang*, J Ba, R Grosse International Conference on Learning Representations (ICLR 2021), 2021 | 68 | 2021 |
| Magnushammer: A transformer-based approach to premise selection M Mikuła, S Tworkowski, S Antoniak, B Piotrowski, AQ Jiang, JP Zhou, ... arXiv preprint arXiv:2303.04488, 2023 | 65* | 2023 |
| Multilingual mathematical autoformalization AQ Jiang, W Li, M Jamnik arXiv preprint arXiv:2311.03755, 2023 | 62* | 2023 |
| Magistral A Rastogi, AQ Jiang, A Lo, G Berrada, G Lample, J Rute, J Barmentlo, ... arXiv preprint arXiv:2506.10910, 2025 | 30 | 2025 |
| End-to-end ontology learning with large language models A Lo, AQ Jiang, W Li, M Jamnik Advances in Neural Information Processing Systems 37, 87184-87225, 2024 | 27 | 2024 |
| Voxtral AH Liu, A Ehrenberg, A Lo, C Denoix, C Barreau, G Lample, JM Delignon, ... arXiv preprint arXiv:2507.13264, 2025 | 25* | 2025 |
| More Details, Please: Improving Autoformalization with More Detailed Proofs G Tarrach, AQ Jiang, D Raggi, W Li, M Jamnik AI for Math Workshop@ ICML 2024, 2024 | 8 | 2024 |
| Repurposing Language Models into Embedding Models: Finding the Compute-Optimal Recipe A Ziarko*, AQ Jiang*, B Piotrowski, W Li, M Jamnik, P Miłoś arXiv preprint arXiv:2406.04165, 2024 | 5* | 2024 |
| Premise Selection for a Lean Hammer T Zhu, J Clune, J Avigad, AQ Jiang, S Welleck arXiv preprint arXiv:2506.07477, 2025 | 3 | 2025 |
| Devstral: Fine-tuning Language Models for Coding Agent Applications A Rastogi, A Yang, AQ Jiang, AH Liu, A Sablayrolles, A Héliou, A Martin, ... arXiv preprint arXiv:2509.25193, 2025 | 2 | 2025 |
Mateja JamnikProfessor of Artificial Intelligence, University of CambridgeVerified email at cam.ac.uk
