![[ICO]](/icons/blank.gif){kind=icon}
![[PARENTDIR]](/icons/back.gif){kind=icon}
![[ ]](/icons/unknown.gif){kind=icon}
![[ ]](/icons/layout.gif){kind=icon}
![[DIR]](/icons/folder.gif){kind=icon}
![[TXT]](/icons/text.gif){kind=icon}
| Name | Last modified | Size | Description |
|---|---|---|---|---|
| Parent Directory | - | ||
| CbmsDemo.lean | 2025-10-26 20:03 | 1.3K | |
| ICARM_introduction.pdf | 2025-10-26 20:03 | 1.9M | |
| ICARM_introduction_m..> | 2025-10-26 20:03 | 1.1M | |
| PartialInstanceGraph..> | 2025-10-26 20:03 | 87K | |
| R2SR.pdf | 2025-10-26 20:03 | 347K | |
| admissible.pdf | 2025-10-26 20:03 | 107K | |
| admissible2.pdf | 2025-10-26 20:03 | 101K | |
| ai4math.pdf | 2025-10-26 20:03 | 1.7M | |
| ai4mathematicians.pdf | 2025-10-26 20:03 | 110K | |
| ams_design.pdf | 2025-10-26 20:03 | 204K | |
| asl04.pdf | 2025-10-26 20:03 | 213K | |
| asl_promise.pdf | 2025-10-26 20:03 | 1.5M | |
| australia1.pdf | 2025-10-26 20:03 | 612K | |
| australia2.pdf | 2025-10-26 20:03 | 120K | |
| australia3.pdf | 2025-10-26 20:03 | 227K | |
| australia4.pdf | 2025-10-26 20:03 | 186K | |
| baltimore.pdf | 2025-10-26 20:03 | 225K | |
| beijing.pdf | 2025-10-26 20:03 | 142K | |
| berkeley_modularity.pdf | 2025-10-26 20:03 | 184K | |
| birs.pdf | 2025-10-26 20:03 | 156K | |
| bohemian.pdf | 2025-10-26 20:03 | 165K | |
| brussels_dirichlet.pdf | 2025-10-26 20:03 | 170K | |
| calgary.pdf | 2025-10-26 20:03 | 1.3M | |
| cbms.pdf | 2025-10-26 20:03 | 105K | |
| clarke.pdf | 2025-10-26 20:03 | 47K | |
| dagstuhl.pdf | 2025-10-26 20:03 | 174K | |
| dagstuhl_2013.pdf | 2025-10-26 20:03 | 132K | |
| dc.pdf | 2025-10-26 20:03 | 112K | |
| decision_procedures.pdf | 2025-10-26 20:03 | 94K | |
| dedekind.pdf | 2025-10-26 20:03 | 512K | |
| definitions2.pdf | 2025-10-26 20:03 | 78K | |
| design.pdf | 2025-10-26 20:03 | 200K | |
| digital_revolution2.pdf | 2025-10-26 20:03 | 5.1M | |
| dirichlet.pdf | 2025-10-26 20:03 | 358K | |
| distances.pdf | 2025-10-26 20:03 | 88K | |
| education.pdf | 2025-10-26 20:03 | 143K | |
| euclid.pdf | 2025-10-26 20:03 | 3.9M | |
| fields_education.pdf | 2025-10-26 20:03 | 175K | |
| fields_hott.pdf | 2025-10-26 20:03 | 169K | |
| fields_hott_lean.pdf | 2025-10-26 20:03 | 510K | |
| fields_type_theory.pdf | 2025-10-26 20:03 | 221K | |
| fmtea.pdf | 2025-10-26 20:03 | 229K | |
| forcing.pdf | 2025-10-26 20:03 | 106K | |
| forcing_talk2.pdf | 2025-10-26 20:03 | 116K | |
| geometry.pdf | 2025-10-26 20:03 | 476K | |
| heidelberg.pdf | 2025-10-26 20:03 | 140K | |
| helsinki/ | 2025-10-26 20:03 | - | |
| herbrand2.pdf | 2025-10-26 20:03 | 93K | |
| him_stark.pdf | 2025-10-26 20:03 | 414K | |
| hoskinson_inaugural.pdf | 2025-10-26 20:03 | 459K | |
| icerm.pdf | 2025-10-26 20:03 | 130K | |
| icerm_2016.pdf | 2025-10-26 20:03 | 215K | |
| ijcar.pdf | 2025-10-26 20:03 | 404K | |
| illinois_understandi..> | 2025-10-26 20:03 | 230K | |
| interpreting.pdf | 2025-10-26 20:03 | 88K | |
| inverting2.pdf | 2025-10-26 20:03 | 125K | |
| ioannina.pdf | 2025-10-26 20:03 | 261K | |
| karlsruhe.pdf | 2025-10-26 20:03 | 2.8M | |
| kerala.pdf | 2025-10-26 20:03 | 2.5M | |
| lausanne.pdf | 2025-10-26 20:03 | 238K | |
| lean_ini.pdf | 2025-10-26 20:03 | 224K | |
| leiden.pdf | 2025-10-26 20:03 | 130K | |
| london.pdf | 2025-10-26 20:03 | 281K | |
| london_ergodic_theor..> | 2025-10-26 20:03 | 156K | |
| loughborough.pdf | 2025-10-26 20:03 | 170K | |
| loughborough2.pdf | 2025-10-26 20:03 | 259K | |
| manchester.pdf | 2025-10-26 20:03 | 199K | |
| math_concepts.pdf | 2025-10-26 20:03 | 248K | |
| mathematical_compone..> | 2025-10-26 20:03 | 702K | |
| mathematical_practic..> | 2025-10-26 20:03 | 54K | |
| mechanization.pdf | 2025-10-26 20:03 | 1.3M | |
| mechanization_talk.pdf | 2025-10-26 20:03 | 1.3M | |
| mechanization_talk_o..> | 2025-10-26 20:03 | 1.2M | |
| mit.pdf | 2025-10-26 20:03 | 156K | |
| munich_dirichlet.pdf | 2025-10-26 20:03 | 211K | |
| newyork.pdf | 2025-10-26 20:03 | 130K | |
| nonstandard2.pdf | 2025-10-26 20:03 | 94K | |
| obsolete.pdf | 2025-10-26 20:03 | 819K | |
| obsolete2.pdf | 2025-10-26 20:03 | 3.1M | |
| ohio_convergence.pdf | 2025-10-26 20:03 | 202K | |
| oxford_formal_method..> | 2025-10-26 20:03 | 287K | |
| paris.pdf | 2025-10-26 20:03 | 96K | |
| paris_functions.pdf | 2025-10-26 20:03 | 164K | |
| pasadena.pdf | 2025-10-26 20:03 | 739K | |
| perimeter_surveillan..> | 2025-10-26 20:03 | 184K | |
| pitt.pdf | 2025-10-26 20:03 | 132K | |
| poland.pdf | 2025-10-26 20:03 | 362K | |
| polya.pdf | 2025-10-26 20:03 | 202K | |
| prague.pdf | 2025-10-26 20:03 | 196K | |
| princeton.pdf | 2025-10-26 20:03 | 579K | |
| proof_systems.pdf | 2025-10-26 20:03 | 224K | |
| proofsociety.pdf | 2025-10-26 20:03 | 559K | |
| qpf.pdf | 2025-10-26 20:03 | 175K | |
| quarantine.pdf | 2025-10-26 20:03 | 171K | |
| rademacher1-intro.pdf | 2025-10-26 20:03 | 4.4M | |
| rademacher2-formaliz..> | 2025-10-26 20:03 | 4.4M | |
| rademacher3-automate..> | 2025-10-26 20:03 | 3.4M | |
| rademacher4-machine-..> | 2025-10-26 20:03 | 4.2M | |
| realizability.pdf | 2025-10-26 20:03 | 57K | |
| reliability_talk.pdf | 2025-10-26 20:03 | 100K | |
| rutgers.pdf | 2025-10-26 20:03 | 533K | |
| san_diego.pdf | 2025-10-26 20:03 | 376K | |
| sc_square.pdf | 2025-10-26 20:03 | 236K | |
| semantic.pdf | 2025-10-26 20:03 | 128K | |
| sheaves.pdf | 2025-10-26 20:03 | 87K | |
| simplicity.pdf | 2025-10-26 20:03 | 79K | |
| sledgehammer.pdf | 2025-10-26 20:03 | 3.4M | |
| spain.pdf | 2025-10-26 20:03 | 72K | |
| stanford.pdf | 2025-10-26 20:03 | 96K | |
| stanford_formal_meth..> | 2025-10-26 20:03 | 444K | |
| stanford_understandi..> | 2025-10-26 20:03 | 579K | |
| stark_cpp.pdf | 2025-10-26 20:03 | 187K | |
| steinhaus.htm | 2025-10-26 20:03 | 1.1K | |
| structures.pdf | 2025-10-26 20:03 | 408K | |
| structures_old.pdf | 2025-10-26 20:03 | 223K | |
| survey1.pdf | 2025-10-26 20:03 | 107K | |
| sweden.pdf | 2025-10-26 20:03 | 122K | |
| tautologies.pdf | 2025-10-26 20:03 | 72K | |
| thedu.pdf | 2025-10-26 20:03 | 215K | |
| topos.pdf | 2025-10-26 20:03 | 513K | |
| toulouse1.pdf | 2025-10-26 20:03 | 127K | |
| toulouse2.pdf | 2025-10-26 20:03 | 169K | |
| toulouse3.pdf | 2025-10-26 20:03 | 259K | |
| toulouse4.pdf | 2025-10-26 20:03 | 420K | |
| toulouse5.pdf | 2025-10-26 20:03 | 180K | |
| type_inference.pdf | 2025-10-26 20:03 | 156K | |
| ud_talk.pdf | 2025-10-26 20:03 | 135K | |
| understanding2022.pdf | 2025-10-26 20:03 | 229K | |
| updatetalk.pdf | 2025-10-26 20:03 | 116K | |
| varieties_small.pdf | 2025-10-26 20:03 | 3.9M | |
| varieties_talk.pdf | 2025-10-26 20:03 | 4.0M | |
| varieties_talk_hando..> | 2025-10-26 20:03 | 4.0M | |
| verification.pdf | 2025-10-26 20:03 | 71K | |
| vienna.pdf | 2025-10-26 20:03 | 101K | |
| vig.pdf | 2025-10-26 20:03 | 124K | |
| wesley.pdf | 2025-10-26 20:03 | 421K | |
| wkl_seminar.pdf | 2025-10-26 20:03 | 187K | |
| wuhan.pdf | 2025-10-26 20:03 | 173K | |