Skip to main content
Proof Assistants Beta
Mike Shulman's user avatar
Mike Shulman's user avatar
Mike Shulman's user avatar
Mike Shulman
  • Member for 2 years, 10 months
  • Last seen more than a week ago
Profile Activity

19 Answers

Score Activity Newest
43 votes

Has anyone ever accidentally "proven" a false theorem with type-in-type?

18 votes

When to use coinductive types?

17 votes
Accepted

What are the motivations for different variants of categorical models of dependent type?

16 votes

How to represent mathematical partial functions in a type-theory based proof assistant?

16 votes

What are some examples of proof assistants doing something useful?

11 votes

What set-theoretic definitions can't easily be formalized in a type theory?

11 votes
Accepted

Type Checking Undecidable in Extensional Type Theory

10 votes
Accepted

What are the advantages of normalization by evaluation over traditional reduction-based normalization?

8 votes

What about dependent types is useful for theorem provers?

8 votes
Accepted

Ergonomic use of multicategories in proof assistants

6 votes

To what extent is formalized mathematics publishable?

6 votes

Finding symbols in Lean

6 votes

Examples of new mathematics discovered through formalization?

5 votes
Accepted

How to state and prove the associativity of append of sized vectors with homogeneous equality?

5 votes

Why are impredicative constructions used less in type theory than in material set theory?

4 votes
Accepted

When is hProp equivalent to the subobject classifier?

3 votes
Accepted

List of general purpose Coq sublanguages for defining custom tactics

3 votes

Counterexamples in Type Theory

2 votes

Generic proof assistants/modularity of the proof assistants?