Thomas Zhu
Thomas Zhu has 2 papers in our library, in 2024–2025, most of them on Reasoning; often with Sean Welleck, Albert Q. Jiang, Jeremy Avigad.
OpenAlex · ORCID · h-index 1 · 6 works · 1 citations OpenAlex, 2026-10-14
📄 2 works in our library · 🔗 Cited 22 times in our library · ⭐ Paper Stars ranking: #10906
Affiliations
Fields, topics and concepts
📚 Shelves 3The field of science this work belongs to (OpenAlex fields).Computer Science · 2 worksArtificial Intelligence · 2 worksComputational Theory and Mathematics · 2 works
🧭 Topics 1Research subjects and languages the work is about.Reasoning · 1 work
Works by year
2020s
Papers
- miniCTX: Neural Theorem Proving with (Long-)Contexts (2024 · 18 citations)
Most neural theorem provers see only the current proof state. They are tested on self-contained competition problems or on library theorems they may already have seen during training. Real formalization work is different: proofs rely on definitions, lemmas, notation and comments introduced earlier in the same… - Premise Selection for a Lean Hammer (2025 · 5 citations)
Lean users often have to name, by hand, the exact lemmas that justify each small proof step, drawn from libraries with hundreds of thousands of facts.
Co-authors here
Cited by
Updated
This page in Markdown → https://md.research.elamur.ai/free/en/authors/thomas-zhu/