Curriculum vitae
My research interests are model theory and mathematical logic; formalized mathematics and automated theorem proving; and visual and category-theoretic approaches to formal languages.
Education
Ph.D. in Mathematics (incoming)
Primary supervisor: Pantelis Eleftheriou
Secondary supervisor: Vincenzo L. Mantova
M.Sc. in Mathematics
Thesis: VC-density in pairs of strongly minimal structures
Advisor: Ayhan Günaydın
Selected coursework: O-minimal theories, applications of model theory to number theory, algebraic number theory, modern algebraic geometry, algebraic topology II, computational complexity theory, functional programming, logic for computer science, and software verification.
B.S. in Electrical and Electronics Engineering
Senior project: Synchronization in several coupled van der Pol oscillators
Advisor: Yağmur Denizhan
Selected coursework: linear multivariable systems theory, chaotic dynamics, nonlinear control, signal processing, functional analysis, representation theory, algebraic topology I, measure theory, and algebra I & II.
B.S. in Physics
Selected coursework: Lie groups and Lie algebras, statistical mechanics, relativistic electromagnetic theory, and quantum mechanics.
Research experience
Project course: Formalizing Quantifier Elimination in Lean
Collaborated with four undergraduate students and Ayhan Günaydın on formalizing quantifier-elimination results in Lean.
- Formalized the back-and-forth method for quantifier elimination.
- Applied the formalized method to prove that the theory of dense linear orders without endpoints admits quantifier elimination.
Undergraduate Research Assistant
Supervisor: Ender Konukoğlu
- Studied the spatial inductive bias of convolutional neural networks in the Deep Image Prior framework.
- Helped develop a training-free, image-specific neural architecture search method by formulating metrics, designing experiments, developing most of the codebase, and writing the manuscript.
- The work was accepted at CVPR 2022.
Undergraduate Research Assistant
Supervisor: Ahmet Öncü
- Developed graphical interfaces for programming digital circuits.
- Contributed to digital circuit design and verification.
Publication
Metin Ersin Arıcan*, Özgür Kara*, Gustav Bredell, and Ender Konukoğlu. “ISNAS-DIP: Image-Specific Neural Architecture Search for Deep Image Prior.” In Proceedings of the IEEE/CVF Conference on Computer Vision and Pattern Recognition (CVPR), 1960–1968, 2022. Paper
* Equal contribution.
Teaching
Graduate Teaching Assistant
MATH 412 (Introduction to Axiomatic Set Theory), MATH 411 (Introduction to Mathematical Logic), MATH 323 (Rings, Fields and Galois Theory), MATH 222 (Group Theory), MATH 201 (Linear Algebra), MATH 105 (Introduction to Finite Mathematics), MATH 102 (Calculus II), and MATH 101 (Calculus I).
Physics Instructor
Delivered lectures and problem-solving sessions in electromagnetism, mechanics, and modern physics to nominees for Turkey’s national physics olympiad team.
Professional experience
Data & Machine Learning Engineer / AI Tutor
Prepared a formal mathematics dataset for training large language models on autoformalization and automated theorem proving.
Cryptanalyst Intern
- Prepared technical presentations and reports on linear and differential cryptanalysis of DES-like block ciphers, and implemented the algorithms from scratch in Python.
- Presented Grover’s and Shor’s algorithms and their applications to breaking RSA.
- Prepared reports on lattice-based cryptography and the Fiat–Shamir transform.
R&D Intern
- Studied voice activity detection using recurrent neural networks and handcrafted features.
- Designed experiments and benchmarks for comparing state-of-the-art voice activity detection systems.
Workshops & programs
- Mentor, Directed Reading Program Turkey · Jun–Aug 2024. Mentored a third-year mathematics student at Middle East Technical University on enriched categories, abelian categories, and Mitchell’s embedding theorem.
- School on Formal Mathematics, Hausdorff Institute · May 2024. Worked on a Fourier theory formalization project in Lean led by Floris van Doorn.
- eCHT Homotopy Theory Course · Jan–May 2024. Completed an online course on homotopy theory taught by Jack H. Carlisle.
- Participant, Directed Reading Program Turkey · Jun–Aug 2023. Studied categorical logic and topos theory with Praneet Srivastava, wrote a report, and gave a concluding talk at Sabancı University.
- Reading Program, Boğaziçi University · Apr–Sep 2022. Studied mathematical logic and axiomatic set theory with Betül Tanbay and gave a concluding talk at Boğaziçi University.
Talks
- Formal Mathematics: An Introduction · Feb 2026, Feza Gürsey Institute. Surveyed developments at the intersection of mathematics, artificial intelligence, and formalization; compared ZFC in first-order logic with Martin-Löf type theory; and introduced the core ideas of Martin-Löf type theory.
- An Introduction to Lean for Mathematicians · Dec 2024, Boğaziçi University
- O-minimal Structures and VC-Dimension · Dec 2023, Boğaziçi University
- An Introduction to Categorical Logic and Topoi · Aug 2023, Sabancı University
- Counterexamples in Topology via Ordinals & Cardinals · Dec 2022, Boğaziçi University
Awards & scholarships
- Graduate Scholarship, Turkish Education Foundation (TEV) · 2023–2025
- 2210-E Graduate Scholarship, TÜBİTAK · 2023–2025
- 2205-E Undergraduate Scholarship, TÜBİTAK · 2018–2023
- Finalist, Travel Datathon and Machine Learning Competition, Turkish Airlines · 2019. Finalist among 75 teams.
- 437th place, Turkish National University Entrance Exam · 2018. Ranked 437th among approximately two million candidates.
- Silver Medal, International Physics Olympiad · 2018
- Bronze Medal, European Physics Olympiad · 2018
- Honorable Mention, Asian Physics Olympiad · 2018
- Silver Medal, Turkish Physics Olympiad · 2017
Last updated: August 9, 2026.