| Systems analysis of auxin transport in the Arabidopsis root apex LR Band, DM Wells, JA Fozard, T Ghetiu, AP French, MP Pound, ... The Plant Cell 26 (3), 862-875, 2014 | 229 | 2014 |
| Autoformalization with large language models Y Wu, AQ Jiang, W Li, M Rabe, C Staats, M Jamnik, C Szegedy Advances in Neural Information Processing Systems 35, 32353-32368, 2022 | 152 | 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 | 120 | 2022 |
| 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ś, ... Advances in Neural Information Processing Systems 35, 8360-8373, 2022 | 81 | 2022 |
| IsarStep: a Benchmark for High-level Mathematical Reasoning W Li, L Yu, Y Wu, LC Paulson International Conference on Learning Representations, 2021 | 72 | 2021 |
| LISA: Language models of ISAbelle proofs AQ Jiang, W Li, JM Han, Y Wu 6th Conference on Artificial Intelligence and Theorem Proving, 378-392, 2021 | 62 | 2021 |
| Lime: Learning inductive bias for primitives of mathematical reasoning Y Wu, MN Rabe, W Li, J Ba, RB Grosse, C Szegedy International Conference on Machine Learning, 11251-11262, 2021 | 60 | 2021 |
| Evaluating language models for mathematics through interactions KM Collins, AQ Jiang, S Frieder, L Wong, M Zilka, U Bhatt, T Lukasiewicz, ... Proceedings of the National Academy of Sciences 121 (24), e2318124121, 2024 | 37 | 2024 |
| Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL W Li, GO Passmore, LC Paulson Journal of Automated Reasoning 62 (1), 69-91, 2019 | 21 | 2019 |
| Simple type theory is not too simple: Grothendieck’s schemes without dependent types A Bordg, L Paulson, W Li Experimental Mathematics 31 (2), 364-382, 2022 | 20 | 2022 |
| A formal proof of Cauchy’s residue theorem W Li, LC Paulson Interactive Theorem Proving: 7th International Conference, ITP 2016, Nancy …, 2016 | 18 | 2016 |
| DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data H Xin, D Guo, Z Shao, Z Ren, Q Zhu, B Liu, C Ruan, W Li, X Liang arXiv preprint arXiv:2405.14333, 2024 | 17 | 2024 |
| Decomposing the enigma: Subgoal-based demonstration learning for formal theorem proving X Zhao, W Li, L Kong arXiv preprint arXiv:2305.16366, 2023 | 17 | 2023 |
| A modular, efficient formalisation of real algebraic numbers W Li, LC Paulson Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and …, 2016 | 16 | 2016 |
| Multilingual mathematical autoformalization AQ Jiang, W Li, M Jamnik arXiv preprint arXiv:2311.03755, 2023 | 15 | 2023 |
| Don't Trust: Verify--Grounding LLM Quantitative Reasoning with Autoformalization JP Zhou, CE Staats, W Li, C Szegedy, KQ Weinberger, Y Wu The Twelfth International Conference on Learning Representations, 2023 | 15 | 2023 |
| Modelling high-level mathematical reasoning in mechanised declarative proofs W Li, L Yu, Y Wu, LC Paulson arXiv preprint arXiv:2006.09265, 2020 | 12 | 2020 |
| Evaluating Winding Numbers and Counting Complex Roots through Cauchy Indices in Isabelle/HOL W Li, LC Paulson Journal of Automated Reasoning 64 (2), 331-360, 2020 | 12 | 2020 |
| The Sturm–Tarski theorem W Li Archive of Formal Proofs, 2014 | 7 | 2014 |
| Irrational rapidly convergent series A Koutsoukou-Argyraki, W Li Archive of Formal Proofs, 2018 | 5 | 2018 |
Yuhuai(Tony) WuCo-Founder of xAIVerified email at x.ai
