Andrej Bauer

Member for 1 year, 8 months
Last seen this week

andrej.com
Ljubljana

Summary

Reputation

7,853

7.9k
6.9k
5.9k

Jan
Apr
Jul
Oct

Next tag badge

62/100 score

8/20 answers

Badges

19

58

Newest

coq

Next badge

0/1

Excavator

Answers

View all 97 answers

Score Activity Newest

33

What is predicativity?

Feb 11, 2022

31

In Lean, what do double curly brackets mean?

Feb 8, 2022

30

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

Feb 9, 2022

28

What is an algebraic data type?

Feb 28, 2022

24

Non-trivial difference(s) between Computer Algebra System and Proof Assistant

Feb 8, 2022

Questions

Score Activity Newest Views

6

Speeding up large data structures in Lean

Apr 15

Tags

View all 96 tags

type-theory

191

Score

21

posts

foundations

108

Score

7

posts

coq

104

Score

22

posts

set-theory

74

Score

4

posts

lean

62

Score

8

posts

Reputation

+30

(Dis)Advantages of basing a proof assistant on CH correspondence?

+10

Speeding up large data structures in Lean

+10

What's the difference between reflection and tactics?

+10

How to run Agda?

Badges

View all badges

This user doesn’t have any gold badges yet.

19

silver badges

Pundit

Apr 17, 2022
Good Answer

× 5

Apr 1
Enthusiast

Mar 26, 2022

58

bronze badges

coq

Aug 18
Disciplined

Feb 14, 2022
Revival

× 2

Jun 6

Accounts

View all 18 accounts

46.2k
10
117
225

Computer Science

29.9k
1
70
115

Theoretical Computer Science

28.1k
1
79
130

Proof Assistants

7,853
19
58

2,806
15
22

Active bounties (0)

Active Offered Earned

This user has no active bounties

Votes cast

225

upvotes

50

downvotes

100

question votes

175

answer votes

3

this month

3

this week