Sina Hazratpour

Sina Hazratpour

Publications

PhD Thesis

May 01, 2019

Under supervision of Steve Vickers

Talks And Presentations

A DSL for HoTT in Lean 4

August 01, 2024

Trimester in Prospects of Formal Mathematics, Hausdorff Research Institute in Mathematics (HIM), Bonn

Linear Algebra Game in Lean4

June 19, 2024

Trimester in Prospects of Formal Mathematics, Hausdorff Research Institute in Mathematics (HIM), Bonn

A game to learn linear algebra in Lean4 at Heinrich Heine University, Düsseldorf

Teaching Introduction To Proofs With Lean

January 11, 2023

Seminar Talk, TU Delft Programming Language Group

In Fall 2022, I taught an undergraduate course in the Mathematics Department at Johns Hopkins University entitled “Introduction to Proofs” entirely with the Lean Proof Assistant. In this talk, I will report on this teaching experiment.

Kripke Joyal Semantics For Dependent Type Theory

December 11, 2020

HoTT Seminar, Pittsburgh HoTT Seminar

The result here was earlier presented at the Yorkshire and Midlands Category Theory Seminars (YaMCATS) and Ghent–Leeds Virtual Logic Seminar and also at CATS seminars at ILLC, UvA, Amsterdam.

Topology Seminar at Johns Hopkins (2021-2022)

With Maru Sarazola and Tim Campion we are organizing Topology Seminar at Johns Hopkins

Reading Group on Arithmetic Universes (2018-2019)

With Alexander Oldenziel, Joost van Dijk and a few others we have an informal weekly reading sessions on Arithmetic Universes and Goedel's incompleteness theorem in Utrecht and Amsterdam.

CARGO (2016-2019)

I am one of the organizers of category theory reading group (CARGO). The meetings takes place at the school of computer science on a weekly basis. The participants are mostly PhD students and research fellows in theoretical computer science.

Read more about it here .

  • From 2015-2017, CARGO meetings used to takes place at the school of computer science on every Tuesday at 2:00 p.m. in room 245. For the academic year of 2017-2018 we have our meetings on Thursdays at 11:00 a.m. in the same room.
  • Here is the archive of talks: CARGO archive. Feel free to subscribe to our mailing list. Let me also mention the archive of our Theory Seminars talks on Fridays. I have given four talks in theory seminars and numerous talks in CARGO. Sometimes I find enough time and I write the notes of the talks which can be found in below.
  • Here is a list of topics considered to be discussed in Autumn 2017 in Category Reading Group seminars as well as informal archive for suggested topics since Summer 2015: Potential topics and Informal archive.

Expository Papers And Notes

Writing notes helps me to grasp a mathematical concept or construction and they become less elusive in my mind. Here are the notes from some of my talks for which I had time to type them up. Any reports of mistakes and errors from the reader are always welcome.

A topos without points

Published:

An example of a topos (from logic) that does not have any points.

A learning wishlist

Published:

A list of tricks/theorems/constructions/concepts/theories I wished to know but never had time/opportunity to learn them!

Principal Bundles

Incomplete as they stand (April, 2018)

A review of theory of principal bundles and higher principal bundles

Principal Bundles

Incomplete as they stand (April, 2018)

A review of theory of principal bundles and higher principal bundles

Three Sites Of Relative Schemes

Incomplete as they stand (April, 2018)

Warning: in construction! We introduce three Grothendieck topologies on the category of based schemes; the Zariski, the étale and the fpqc topology