1,151 reputation
410
bio website andrej.com
location Slovenia
age
visits member for 2 years, 2 months
seen 2 days ago

Jul
6
comment Big Challenge in TM & R.E Set
Not worth it, it's just a typo.
Jul
5
answered What kind of math can be formalized in first order logic using PA axioms?
Jul
5
comment Big Challenge in TM & R.E Set
The two sentences are different because the second one is wrong.
Jun
17
answered A bounded sequence in $C[a,b]$ (normed by maximum norm) that has no convergent subsequence
Jun
10
comment Why can almost all ordinary mathematics be formalized by sets?
Well, I can't argue against your personal experience. I am reporting on what the community around me is using. Mizar seems to be used by a fairly closed community, I know very little about Metamath. Also, in what sense are Mizar and Metamath proof assistants? They are proof checkers.
May
5
awarded  Yearling
Apr
5
awarded  Nice Answer
Mar
19
comment Countable axiom of choice: why you can't prove it from just ZF
The other way to read the construction of $C(n)$ is that he used dependent choice. That would actually give the desired sequence of $C(n)$'s.
Mar
19
comment Countable axiom of choice: why you can't prove it from just ZF
On the other hand, a typical research mathematician cannot tell where @Divakar used choice in his argument.
Mar
19
answered Countable axiom of choice: why you can't prove it from just ZF
Feb
17
answered Two circles intersect in two points
Feb
17
comment Two circles intersect in two points
Note that solitions at $\infty$ also count, and that you have to take into account multiplicities of zeros (although that does not seem to be an issue here).
Feb
17
comment Two circles intersect in two points
For example by providing these complex points. Mathematica cannot find them.
Feb
15
comment Constructive proof for: P => ((P => Q) => Q)
"Assume $P$. Assume $P \Rightarrow Q$. From $P$ and $P \Rightarrow Q$ it follows that $Q$. QED."
Feb
9
awarded  Enlightened
Feb
8
comment Continuity from complete metric space
Oops, there was a typo. It should be $|2^{-m} - 2^{-n}|$. Fixed, thanks for catching it.
Feb
8
revised Continuity from complete metric space
typo
Feb
7
answered Continuity from complete metric space
Feb
5
awarded  Nice Answer
Feb
5
comment Why can almost all ordinary mathematics be formalized by sets?
It is a fact that actual formalizations of mathematics tend to use types rather than sets. This is extremely strong evidence in favor of the position that sets are not more primitive. Anyone arguing otherwise must explain this phenomenon.