12,112 reputation
340112
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
I'm just here for asking stupid questions.

4h
comment Errata for Atiyah-Macdonald
$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(p-r\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 pre-existing 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}^{n-1} C_i C_{n-1-i}$. Indeed, the right hand side of (1) does not change if I replace $4i+3$ by $4\left(n-1-i\right)+3$ (because this is tantamount to substituting $n-1-i$ for $i$ in the sum). Therefore it also does not change if I replace $4i+3$ by $\left(4i+3\right)+\left(4\left(n-1-i\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}^{n-1} C_i C_{n-1-i}$, 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 Atiyah-Macdonald
fixing broken latex