Elamur Research⌕
☰
home / authors / Bartosz Piotrowski

Bartosz Piotrowski

Bartosz Piotrowski has 5 papers in our library, in 2019–2023, most of them on Reasoning; often with Josef Urban, Albert Q. Jiang, Christian Szegedy.

5 papers in our library · 2019–2023

OpenAlex · ORCID · h-index 7 · 19 works · 128 citations OpenAlex, 2026-10-14

📄 5 works in our library · 🔗 Cited 172 times in our library · ⭐ Paper Stars ranking: #6146

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

🎓University of WarsawWarsaw · Poland2018–2025 · 12 paperscurrent🎓Czech Technical University in PraguePrague · Czechia2020–2023 · 6 papers

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

 Fields, topics and concepts

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

📚 Shelves 6The field of science this work belongs to (OpenAlex fields).Computer Science · 5 worksArtificial Intelligence · 5 worksComputational Theory and Mathematics · 3 worksArts and Humanities · 1 workLanguage and Linguistics · 1 workMathematics · 1 work

🧭 Topics 1Research subjects and languages the work is about.Reasoning · 3 works

 Works by year

2020s

20232 papers20202 papers

2010s

20191 paper

 Papers

The most cited first (OpenAlex and our library).

  1. ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics (2023 · 142 citations)
    Autoformalization means converting informal mathematics into statements a proof assistant can check. Progress has been limited by the scarcity of paired informal and formal data. Existing prover benchmarks also lean on competition problems that require only a small set of elementary facts. To address this, the…
  2. ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (system description) (2020 · 42 citations)
    Learned guidance for saturation-style provers usually relies on symbol names. Such guidance cannot carry over to problems or libraries that use different names. This system description adds two name-agnostic clause classifiers to the ENIGMA framework of the E prover. Under either classifier, consistently renaming all…
  3. Magnushammer: A Transformer-Based Approach to Premise Selection (2023 · 35 citations)
    Premise selection means picking, from a large library of proven facts, the few that help close the current goal in a formal proof.
  4. Stateful Premise Selection by Recurrent Neural Networks (2020 · 21 citations)
    Automated theorem provers that work over large formal libraries depend on premise selection, which means picking the few relevant facts from thousands of candidates.
  5. Guiding Inferences in Connection Tableau by Recurrent Neural Networks (2019 · 15 citations)
    Connection-style theorem provers such as leanCoP must repeatedly decide which input clause to use when extending an open branch of the proof tree.

 Co-authors here

12 of 17 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 172 times (of the 149,439 papers whose bibliographies we read); 78 citing papers with a page here →.

Updated

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