bio  website  mit.edu/~darij/www 

location  Karlsruhe (home), Munich (until summer 2011), Cambridge/MA (2011)  
age  26  
visits  member for  5 years, 6 months 
seen  1 min ago  
stats  profile views  12,539 
I'm just here for asking stupid questions.
4h

comment 
Errata for AtiyahMacdonald
$D = d$ in your last remark? 
5h

comment 
What technical and/or theoretical challenges are involved in automatically extracting proofs from books and papers into Coq code?
@AndrejBauer: thank you! 
6h

comment 
Which colimits commute with which limits in the category of sets?
Nope, and I'm also interested in it. 
9h

comment 
Which colimits commute with which limits in the category of sets?
@Arrow: This is not the thesis, though. 
20h

comment 
Is Zsigmondy's Theorem utilized in Sociology to the extent that a lay person might be familiar with its use?
Why should Zsigmondy's theorem (a result in number theory, if we are talking about the same Zsigmondy's theorem) be used in sociology? This is missing context... 
20h

answered  Proving inequation with ceilings in Finite Field of characteristic $p$ 
20h

comment 
Proving inequation with ceilings in Finite Field of characteristic $p$
Are you sure you mean $u\left(pr\right) \equiv 1 \mod p$ ? The first $p$ looks redundant. 
1d

revised 
commutative algebra, diagonal morphism
minor correction (I was meant to be I') and clarifications 
1d

revised 
commutative algebra, diagonal morphism
disambiguation for "algebra" 
1d

revised 
Equivalence of “Weyl Algebra” and “Crystalline” definitions of rings of differential operators between modules?
typos II 
1d

revised 
Equivalence of “Weyl Algebra” and “Crystalline” definitions of rings of differential operators between modules?
typo 
1d

comment 
What technical and/or theoretical challenges are involved in automatically extracting proofs from books and papers into Coq code?
... prevented from formalizing their proofs in Coq by such problems than those who genuinely find proof formalization to be beneath them and obscuring. 
1d

comment 
What technical and/or theoretical challenges are involved in automatically extracting proofs from books and papers into Coq code?
I fear I find this somewhat inconcrete. In my limited experience with Coq, I have encountered some rather specific roadblocks, such as lack of documentation (even installation on Linux isn't something I can reliably do), a steep learning curve, and annoyances such as the fact that every other set I need is really a setoid and I'd have to learn a whole new yoga to work with them (without really having much preexisting knowledge to learn from, since everyone else seems to either avoid the need for setoids or assume univalence to get rid of it). I think there are far more people who are ... 
1d

comment 
What technical and/or theoretical challenges are involved in automatically extracting proofs from books and papers into Coq code?
... means much); in its purest form, it assumes that computers already have a good grasp of the form of logical reasons that mathematicians use and only have difficulties with the terseness of their writing. Counterintuitively, it appears to me that (2) is simpler than (1), given how good Coq's automation and SSReflect's reflection are at filling in straightforward steps. 
1d

comment 
What technical and/or theoretical challenges are involved in automatically extracting proofs from books and papers into Coq code?
The problem is really a composition of two problems: (1) How difficult is it to formalize real mathematical proofs for a person who perfectly understands the proof and the proof assistant?, and (2) How difficult is it for a computer to parse a proof written for humans, essentially guessing the missing steps and filling in the gaps left to the reader? Question (1) is about logic and programming paradigms (in particular, about our still imperfect understanding of constructivism and the tacit uses of univalence). Question (2) is an AI question (probably the simplest AI question, not that this ... 
Jul 4 
comment 
A question about a specific inverse proposition of Combinatorial Nullstellensatz
The HNS and the CNS have little to do with each other. 
Jul 3 
comment 
Are there any books that take a 'theorems as problems' approach?
+1. Little bugreport: on page 1, "exercises.pdf" should be "exo.pdf". Also, if you use the hyperref package and the \href and \url commands, the links will become clickable. 
Jul 3 
comment 
Identities involving sums of Catalan numbers
(1) is a fairly simple equivalent form of the standard recurrence $C_n = \sum_{i=0}^{n1} C_i C_{n1i}$. Indeed, the right hand side of (1) does not change if I replace $4i+3$ by $4\left(n1i\right)+3$ (because this is tantamount to substituting $n1i$ for $i$ in the sum). Therefore it also does not change if I replace $4i+3$ by $\left(4i+3\right)+\left(4\left(n1i\right)+3\right) = 4n+2$ and then divide the whole sum by $2$. But if I do that, the right hand side becomes $\left(4n+2\right) \sum_{i=0}^{n1} C_i C_{n1i}$, and then everything boils down to the standard recurrence. 
Jul 2 
revised 
Are there any books that take a 'theorems as problems' approach?
update links 
Jul 1 
revised 
Errata for AtiyahMacdonald
fixing broken latex 