Proof Assistants Beta
Mike Shulman's user avatar
Mike Shulman's user avatar
Mike Shulman's user avatar
Mike Shulman
  • Member for 1 year, 10 months
  • Last seen more than a month ago
Profile Activity
Stats
2,912
reputation
13k
reached
19
answers
8
questions
Communities
View all
About

I am an associate professor of mathematics at the University of San Diego. My research is in homotopy type theory and higher category theory.

Badges
View all badges
This user doesn’t have any gold badges yet.
4
silver badges
30
bronze badges
Top tags
View all tags
78
Score
7
Posts
26
Posts %
50
Score
10
Posts
37
Posts %
21
Score
4
Posts
15
Posts %
21
Score
2
Posts
7
Posts %
18
Score
3
Posts
11
Posts %
17
Score
2
Posts
7
Posts %
Top posts
View all questions and answers
All Questions Answers
Score Newest
answer
43
Has anyone ever accidentally "proven" a false theorem with type-in-type?
Apr 1, 2022
question
22
Categorical semantics of Agda
Dec 11, 2022
answer
18
When to use coinductive types?
Feb 9, 2022
answer
17
What are the motivations for different variants of categorical models of dependent type?
Mar 18, 2022
answer
16
How to represent mathematical partial functions in a type-theory based proof assistant?
Feb 16, 2022
answer
15
What are some examples of proof assistants doing something useful?
Feb 8, 2022
question
13
Tutorial implementations of NbE
Mar 16, 2022
question
12
Rules for mutual inductive/coinductive types
Mar 6, 2022
question
10
Universe inconsistency as an effect
Dec 16, 2022
question
10
Uses of first-class implicit function types
Dec 5, 2022
Top Meta posts
1
4
15
Low-quality tags
11
Now that we have our first wiki answer should all the other answers be combined into one?
10
Does [theorem-proving] need to exist?
6
Should there be a mathlib tag for Lean?
4
Why is a question about dependent type theory off topic?
Top network posts
View all network posts
214
Why doesn't mathematics collapse even though humans quite often make mistakes in their proofs?
104
What properties make $[0,1]$ a good candidate for defining fundamental groups?
91
Has incorrect notation ever led to a mistaken proof?
67
Can skeleta simplify category theory?
61
What packages do people load by default in LaTeX?

Your privacy

By clicking “Accept all cookies”, you agree Stack Exchange can store cookies on your device and disclose information in accordance with our Cookie Policy.