| Text and code embeddings by contrastive pre-training A Neelakantan, T Xu, R Puri, A Radford, JM Han, J Tworek, Q Yuan, ... arXiv preprint arXiv:2201.10005, 2022 | 230 | 2022 |
| Formal mathematics statement curriculum learning S Polu, JM Han, K Zheng, M Baksys, I Babuschkin, I Sutskever arXiv preprint arXiv:2202.01344, 2022 | 101 | 2022 |
| Proof Artifact Co-training for Theorem Proving with Language Models JM Han, J Rute, Y Wu, EW Ayers, S Polu arXiv preprint arXiv:2102.06203, 2021 | 67 | 2021 |
| MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics K Zheng, JM Han, S Polu arXiv preprint arXiv:2109.00110, 2021 | 63 | 2021 |
| LISA: Language models of ISAbelle proofs AQ Jiang, W Li, JM Han, Y Wu | 35* | |
| A formal proof of the independence of the continuum hypothesis JM Han, F van Doorn Proceedings of the 9th ACM SIGPLAN International Conference on Certified …, 2020 | 25 | 2020 |
| Unsupervised neural machine translation with generative language models only JM Han, I Babuschkin, H Edwards, A Neelakantan, T Xu, S Polu, A Ray, ... arXiv preprint arXiv:2110.05448, 2021 | 23 | 2021 |
| Enhancing SAT solvers with glue variable predictions JM Han arXiv preprint arXiv:2007.02559, 2020 | 14 | 2020 |
| Contrastive finetuning of generative language models for informal premise selection JM Han, T Xu, S Polu, A Neelakantan, A Radford | 7 | 2021 |
| Towards grounded natural language proof generation S Welleck, J Liu, JM Han, Y Choi MathAI4Ed Workshop at NeurIPS, 2021 | 7 | 2021 |
| A Formalization of Forcing and the Unprovability of the Continuum Hypothesis JM Han, F van Doorn arXiv preprint arXiv:1904.10570, 2019 | 7 | 2019 |
| A formalization of forcing and the consistency of the failure of the continuum hypothesis J Han, F van Doorn International Conference on Interactive Theorem Proving. Springer, Heidelberg 10, 2019 | 6 | 2019 |
| Universal Policies for Software-Defined MDPs D Selsam, JM Han, L de Moura, P Godefroid arXiv preprint arXiv:2012.11401, 2020 | 4 | 2020 |
| Learning cubing heuristics for SAT from DRAT proofs JM Han AITP 2020, 0 | 3* | |
| Automatically Building Diagrams for Olympiad Geometry Problems. R Krueger, JM Han, D Selsam CADE, 577-588, 2021 | 2 | 2021 |
| -Equivalence Relations and Associated Algorithms D Selsam, JM Han arXiv preprint arXiv:2102.04633, 2021 | | 2021 |
| Makkai duality, descent and definability J Han Handbook of the 6th World Congress and School on Universal Logic, 379, 2018 | | 2018 |
| Theories, interpretations, and pretoposes J Han | | 2018 |
| An introduction to abelian sheaf cohomology J Han | | 2018 |
| Strong conceptual completeness for R0-categorical theories J Han | | 2018 |
