Sage Binder

I am a fourth-year CS PhD student in the Computational Logic Center at the University of Iowa, working with Dr. Katherine Kosaian. I have also previously worked with Dr. Aaron Stump. I am interested in formal methods, formalizing mathematics, and the development of proof assistants. I have a bachelor's degree in mathematics from Arizona State University, with a minor in philosophy.

"Is what I am doing really worth the effort? Yes, but only if a light shines on it from above."
—Ludwig Wittgenstein, Culture and Value

Contact

Email: [firstname]-[lastname] [at] uiowa [dot] edu
Mastodon: @SageBinder@mathstodon.xyz
GitHub: SageBinder

Conference Papers

S. Binder, H. Lachnitt, and K. Kosaian. Apply2Isar: Automatically Converting Isabelle/HOL Apply-Style Proofs to Structured Isar. Interactive Theorem Proving (ITP) 2026.
- doi | arXiv | GitHub
- Presented at ITP 2026.
S. Binder, E. Ren, and K. Kosaian. Formalizing the Hidden Number Problem in Isabelle/HOL. Interactive Theorem Proving (ITP) 2025.
- doi | AFP
- Presented at ITP 2025.
S. Binder and K. Kosaian. Formalizing Pick's Theorem in Isabelle/HOL. Conference on Intelligent Computer Mathematics (CICM) 2024.
- doi | arXiv | AFP
- Presented at CICM 2024.

TA Work

Fall 2024 — CS:4980:0003 Theorem Proving in Isabelle/HOL (Professor: Katherine Kosaian)

Internships

Fall 2026 — The Automated Reasoning Group at Amazon (Cambridge, UK)

Service

Subreviewer: CADE 2024, ITP 2026
Student volunteer: NSF FMitF PI Meeting 2024

Awards

Sheets Graduate Fellowship, 2023-24, University of Iowa, CS Department.
Dean's Medalist, Fall 2022, Arizona State University, School of Mathematical and Statistical Sciences (article).