madvorak / fecssk Public

Notifications You must be signed in to change notification settings
Fork 1
Star 12

Formalisms Every Computer Scientist Should Know (course at ISTA)

Unlicense license

12 stars 1 fork Branches Tags Activity

Notifications

Name		Name	Last commit message	Last commit date
Latest commit History 54 Commits
Fecssk		Fecssk
.gitignore		.gitignore
LICENSE		LICENSE
README.md		README.md
lake-manifest.json		lake-manifest.json
lakefile.lean		lakefile.lean
lakefile.olean		lakefile.olean
lean-toolchain		lean-toolchain

Repository files navigation

Formalisms Every Computer Scientist Should Know

Thomas Henzinger teaches this course at ISTA

LaTeX transcribes from the lectures

Timeline

How to Lean 4

Setup Lean

Minimalistic online IDE (no installation needed; just copypaste the code and walk through the proof)

Official installation manual

Learn Lean

Natural Number Game (fun interactive tutorial by Kevin Buzzard et al.)

Overview of basic tactics (things you use in proofs, not definitions)

Code from my minicourse (took place at ISTA in 2023-09)

Code from my tutorial (took place at ISTA in 2024-02)

Some motivation

More motivation

About

Formalisms Every Computer Scientist Should Know (course at ISTA)

Unlicense license

Report repository

Languages

Lean 100.0%