Andrej Bauer

Member for 1 year, 10 months
Last seen this week

andrej.com
Ljubljana

Summary

Reputation

8,222

8.2k
7.3k
6.4k

Mar
Jun
Sep
Dec

Next tag badge

62/100 score

8/20 answers

Badges

20

59

Newest

Enlightened

Next badge

0/1

Excavator

Answers

View all 103 answers

Score Activity Newest

35

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

29

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 100 tags

type-theory

194

Score

21

posts

coq

114

Score

24

posts

foundations

110

Score

7

posts

set-theory

78

Score

5

posts

lean

62

Score

8

posts

Reputation

+10

LEM, the halting problem, the curry-howard correspondence -> deep connection?

+25

In lean4 why is induction only rewriting the goal, and not the known facts?

+10

What is a deep embedding vs a shallow embedding? With examples?

+10

Universe inconsistency errors when using ZF model in Coq

Badges

View all badges

This user doesn’t have any gold badges yet.

20

silver badges

Pundit

Apr 17, 2022
Good Answer

× 5

Apr 1
Enthusiast

Mar 26, 2022

59

bronze badges

coq

Aug 18
Disciplined

Feb 14, 2022
Revival

× 2

Jun 6

Accounts

View all 18 accounts

46.7k
10
120
228

Computer Science

30k
1
70
115

Theoretical Computer Science

28.3k
1
80
130

Proof Assistants

8,222
20
59

2,816
15
22

Active bounties (0)

Active Offered Earned

This user has no active bounties

Votes cast

241

upvotes

55

downvotes

110

question votes

186

answer votes

6

this month

6

this week