Elamur Research⌕
☰
home / authors / Roozbeh Yousefzadeh

Roozbeh Yousefzadeh

Roozbeh Yousefzadeh has 4 papers in our library, in 2024–2025, most of them on Reasoning, Language models & pretraining; often with Azim Ospanov, Farzan Farnia, Haoxiong Liu.

4 papers in our library · 2024–2025

OpenAlex · ORCID · h-index 5 · 34 works · 139 citations OpenAlex, 2026-10-14

📄 4 works in our library · 🔗 Cited 35 times in our library · ⭐ Paper Stars ranking: #10141

The profile is the library's match of the name; two people with one name are not always told apart.

Elsewhere: Google Scholar · Semantic Scholar · dblp · ACL Anthology

 Affiliations

From the bylines of their papers (OpenAlex, 2026-10-14), ORCID and Wikidata; institutions on papers are matched by machine.

 Fields, topics and concepts

Of its works in our library, with the number of works on each.

 Works by year

2020s

 Papers

The most cited first (OpenAlex and our library).

  1. APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning (2025 · 17 citations)
    Automated theorem proving with LLMs usually relies on brute-force sampling: a model writes complete Lean proofs, sometimes thousands of times, and the verifier only reports pass or fail.
  2. Mathesis: Towards Formal Theorem Proving from Natural Languages (2025 · 9 citations)
    Current LLM theorem provers for Lean 4 assume their input is already a formal statement written by an expert. Real problems, however, are stated in natural language. Mathesis targets the full chain from informal problem to verified proof. Its pipeline has three stages:
  3. A Lean Dataset for International Math Olympiad: Small Steps towards Writing Math Proofs for Hard Problems (2024 · 7 citations)
    Formal theorem proving in Lean lacks high-quality reference material. Even miniF2F, the community's standard benchmark, has public formal proofs for only 6 of the 20 IMO problems in its test set. Without reference proofs, it is hard to tell where automated provers go wrong. The authors wrote original Lean 4 proofs…
  4. miniF2F-Lean Revisited: Reviewing Limitations and Charting a Path Forward (2025 · 4 citations)
    This NeurIPS 2025 paper examines miniF2F, a widely used benchmark of 488 competition-style math problems with paired natural-language and Lean statements.

 Co-authors here

6 co-authors with a page, the most papers together first.

Venues

Where their works here were published, the most works first, with the editions of those that have a page.

 Cited by

Papers of our library cite their works 35 times (of the 149,439 papers whose bibliographies we read); 10 citing papers with a page here →.

Updated

This page in Markdown → https://md.research.elamur.ai/free/en/authors/roozbeh-yousefzadeh/