| 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 | 214 | 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 | 93 | 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 | 73 | 2022 |
| IsarStep: a Benchmark for High-level Mathematical Reasoning W Li, L Yu, Y Wu, LC Paulson International Conference on Learning Representations, 2021 | 58 | 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 | 52 | 2021 |
| 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 | 44 | 2022 |
| 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 | 34 | 2021 |
| 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 | 20 | 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 | 16 | 2022 |
| 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 |
| A formal proof of Cauchy’s residue theorem W Li, LC Paulson Interactive Theorem Proving: 7th International Conference, ITP 2016, Nancy …, 2016 | 16 | 2016 |
| Evaluating language models for mathematics through interactions KM Collins, AQ Jiang, S Frieder, L Wong, M Zilka, U Bhatt, T Lukasiewicz, ... arXiv preprint arXiv:2306.01694, 2023 | 14 | 2023 |
| Modelling high-level mathematical reasoning in mechanised declarative proofs W Li, L Yu, Y Wu, LC Paulson arXiv preprint arXiv:2006.09265, 2020 | 11 | 2020 |
| Decomposing the enigma: Subgoal-based demonstration learning for formal theorem proving X Zhao, W Li, L Kong arXiv preprint arXiv:2305.16366, 2023 | 8 | 2023 |
| 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 | 8 | 2020 |
| The Sturm–Tarski theorem W Li Archive of Formal Proofs, 2014 | 7 | 2014 |
| Count the number of complex roots W Li Archive of Formal Proofs, 2017 | 5 | 2017 |
| Multilingual mathematical autoformalization AQ Jiang, W Li, M Jamnik arXiv preprint arXiv:2311.03755, 2023 | 4 | 2023 |
| The transcendence of certain infinite series A Koutsoukou-Argyraki, W Li Archive of Formal Proofs, 2019 | 4 | 2019 |
| Counting polynomial roots in Isabelle/HOL: a formal proof of the Budan-Fourier theorem W Li, LC Paulson Proceedings of the 8th ACM SIGPLAN International Conference on Certified …, 2019 | 4 | 2019 |
Yuhuai(Tony) WuCo-Founder of xAIVerified email at x.ai
