Skip to main content
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, 10 months
  • Last seen more than a week ago
Profile Activity
Stats
660
reputation
7k
reached
12
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
25
Posts %
12
Score
1
Posts
8
Posts %
10
Score
2
Posts
17
Posts %
9
Score
6
Posts
50
Posts %
9
Score
1
Posts
8
Posts %
6
Score
2
Posts
17
Posts %
Top posts
View all questions and answers
answer
12
How usable is Lean for constructive mathematics?
Mar 20, 2022
answer
9
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
130
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?
81
Why is compactness in logic called compactness?
80
What is the high-concept explanation on why real numbers are useful in number theory?