Timeline for Besides proving new theorems, how can a person contribute to mathematics?
Current License: CC BY-SA 3.0
11 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jan 7, 2015 at 14:07 | comment | added | Mario Carneiro | @DavidZhang By the way, for anyone who's interested I maintain a blog chronicling my quest to prove those 100 theorems in Metamath. (40 down, 60 to go!) | |
| Jan 7, 2015 at 13:59 | comment | added | Mario Carneiro | @DavidZhang I literally just discovered Metamath cited on a wiki or maybe here, and read up on it and liked what I saw, so I started writing theorems of my own and sending them in (the maintainer, Norm Megill, is very responsive by email and I just send him stuff that way and it shows up within a few days). Besides the fact that I was exposed to Metamath before other formal systems (the giants in the field are HOL Light, Mizar, Coq and Isabelle), I am quite attracted to the simplicity of Metamath foundations. No other system can claim as direct a connection to the logic textbook approach. | |
| Jan 7, 2015 at 11:38 | comment | added | David Zhang | @MarioCarneiro Fascinating! I had a look at Formalizing 100 Theorems and I am surprised how many well-known results remain unformalized. Can you shed some light on how someone might get started working in this area? What led you to Metamath over other proof checking systems? | |
| Jan 7, 2015 at 11:29 | comment | added | DanielV | @MarioCarneiro Thanks for the edit, I really wish this had existed and I had known about it as an undergrad. | |
| Jan 7, 2015 at 11:05 | history | edited | Mario Carneiro | CC BY-SA 3.0 |
My experience in formal proof
|
| Jan 7, 2015 at 10:47 | comment | added | DanielV | @MarioCarneiro I would appreciate it if you would add to this answer your thoughts and suggestions, I think they would be appreciated by the poster as well. | |
| Jan 7, 2015 at 5:25 | comment | added | Mario Carneiro | @DavidZhang As someone who does exactly this on a regular basis, yes I would absolutely say that you can make a significant original contribution. My first large project was proving Bertrand's postulate in Metamath, and since then I've been invited to a conference, wrote a paper, and I feel like my mathematical career is finally starting to take off. All while still in undergrad. | |
| Jan 4, 2015 at 5:29 | comment | added | rationalis | @DanielV But I mean, how many mathematicians are significant enough to expect the girls at the bar to know their name? I can't think of a single (pun intended) living academic who could walk into an average bar (well, where I live anyways) and expect to be recognized on the merit of their contributions to their field. | |
| Jan 2, 2015 at 17:02 | comment | added | DanielV | @DavidZhang If you look around, possibly. If you are interested I would recommend contacting the authors of a proof wiki and see if there is anything that they would suggest. As far as "significant" goes...I'd say yes probably significant enough to put on a resume, but probably not significant enough to expect the girls at the bar to know your name before you walk in. | |
| Jan 2, 2015 at 16:57 | comment | added | David Zhang | Interesting. Is this proof formalization an area in which a motivated undergraduate could make a significant original contribution? | |
| Jan 2, 2015 at 16:45 | history | answered | DanielV | CC BY-SA 3.0 |