Skip to main content
Proof Assistants Beta
Peter LeFanu Lumsdaine's user avatar
Peter LeFanu Lumsdaine's user avatar
Peter LeFanu Lumsdaine's user avatar
Peter LeFanu Lumsdaine
  • Member for 2 years, 4 months
  • Last seen this week
Profile Activity
Stats
416
reputation
2k
reached
1
answer
2
questions
Communities
View all
About

Mathematician, math.LO/math.CT, currently Associate Professor (Universitetslektor) at Stockholm University. Mainly working in categorical logic, especially homotopy type theory and higher categories.

Previously worked at Institute for Advanced Study, Princeton; Dalhousie University, Halifax, Nova Scotia; and Carnegie Mellon University, Pittsburgh.

Badges
View all badges
This user doesn’t have any gold badges yet.
2
silver badges
8
bronze badges
Top tags
19
Score
1
Posts
33
Posts %
0
Score
2
Posts
67
Posts %
0
Score
1
Posts
33
Posts %
0
Score
1
Posts
33
Posts %
0
Score
1
Posts
33
Posts %
Top posts
19
Is there any example of a dependent product that makes sense in a non-type-theory context?
Mar 21, 2022
6
In VSCoq, how to issue an arbitrary Gallina query via the prompt?
Jul 19, 2022
5
Tools like leanblueprint for other proof assistants, especially Coq?
Jun 7
Top Meta posts
0
1
9
What should the name of our main chatroom be?
Top network posts
View all network posts
401
Pedagogy: How to cure students of the "law of universal linearity"?
289
How do you explain to a 5th grader why division by zero is meaningless?
200
How do I ask for an espresso if there's a good chance they don't know how to make it?
124
Is it unethical to take a photograph of my question sheets from a sit-down exam I've just finished if I am not allowed to take them home?
111
How to deal with a professor who grades assignments and exams incorrectly