Proof Assistants Beta
François G. Dorais's user avatar
François G. Dorais's user avatar
François G. Dorais's user avatar
François G. Dorais
  • Member for 2 years, 2 months
  • Last seen this week
Profile Activity
Stats
625
reputation
5k
reached
11
answers
0
questions
Communities
View all
About

Treasurer for MathOveflow

Department of Mathematics & Statistics, University of Vermont

Badges
View all badges
This user doesn’t have any gold badges yet.
3
silver badges
13
bronze badges
Top tags
View all tags
20
Score
3
Posts
27
Posts %
12
Score
1
Posts
9
Posts %
10
Score
2
Posts
18
Posts %
8
Score
5
Posts
45
Posts %
8
Score
1
Posts
9
Posts %
6
Score
2
Posts
18
Posts %
Top posts
View all questions and answers
answer
12
How usable is Lean for constructive mathematics?
Mar 20, 2022
answer
8
Decidability for an infinite sequence of decidable propositions
Mar 12, 2022
answer
5
How to show in type theory (like in a proof assistant) that finite sets of different cardinalities are not isomorphic?
Jul 8, 2022
answer
5
Cardinality of Type in a given universe
Jul 23, 2022
answer
4
How to represent mathematical partial functions in a type-theory based proof assistant?
May 4, 2022
answer
3
Print the version of lean that is running
Dec 5, 2023
answer
3
Lean and inaccessible cardinals
Feb 12
answer
2
Equality of records with members whose types are dependent (Lean 4)
Sep 22, 2022
answer
2
How to prove the termination of Ackermann in Lean?
May 27, 2023
answer
1
Pattern matching from `Prop` to `Type` in Lean
Jun 4, 2023
Top Meta posts
1
1
7
Low-quality tags
6
Should we have a Citation Helper?
Top network posts
View all network posts
129
explicit big linearly independent sets
127
Proof that pi is transcendental that doesn't use the infinitude of primes
106
What are some examples of colorful language in serious mathematics papers?
80
What is the high-concept explanation on why real numbers are useful in number theory?
77
Why is compactness in logic called compactness?