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
247 2022 Formal mathematics statement curriculum learning S Polu, JM Han, K Zheng, M Baksys, I Babuschkin, I Sutskever
arXiv preprint arXiv:2202.01344, 2022
102 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
69 2021 MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics K Zheng, JM Han, S Polu
arXiv preprint arXiv:2109.00110, 2021
64 2021 LISA: Language models of ISAbelle proofs AQ Jiang, W Li, JM Han, Y Wu
37 * 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 AlgorithmsD 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