7 ms·

This is amazing, no doubt. Not just the craft but the ideas and presentation. However, I can't help but feel uncomfortable that this is not part of 'something

This is amazing, no doubt. Not just the craft but the ideas and presentation. However, I can't help but feel uncomfortable that this is not part of 'something bigger' -as many of the disconnected knowledge pieces across the web- that we could all contribute to (at the least for teaching/sharing/tweaking mathematics). I am talking about a vague idea of what LaTeX was for unifying typesetting but for unifying collaborative proofs+visualization. Call it "VS" [1] to make the following analogy: Before LaTeX, no one would have questioned your thesis for having handwritten equations on the gaps purposely left by you with the typewriter. It would not matter if you penciled the equation in or physically pasted a picture of it. No one would question the choice. Similarly, before this hypothetical VS, people use Matlab, Mathematica, Sage, CoQ etc without anyone questioning any of the choices for a result/proof/visualization. Even worse, before VS++ people publish papers on different journals with different degrees of access, many not even sharing the code used for arriving at such results, no way of verifying/visualizing unless you're running it in your head's OS. [1] https://www.youtube.com/watch?v=KvMxLpce3Xw https://www.youtube.com/watch?v=KvMxLpce3Xw (Vulcan School) [+] I may be repeating myself https://news.ycombinator.com/item?id=11129297 https://news.ycombinator.com/item?id=11129297

Ericson2314 11y ago
Let the field medalist speak. http://www.math.ias.edu/vladimir/files/2010_09_25_slides.pdf http://www.math.ias.edu/vladimir/files/2010_09_25_slides.pdf https://www.math.ias.edu/vladimir/sites/math.ias.edu.vladimir/files/2014_08_ASC_lecture.pdf https://www.math.ias.edu/vladimir/sites/math.ias.edu.vladimi...
- vinchuco 11y ago
  Disregarding speech would be terrible, wouldn't it? Thanks for the pointers.
- fao_ 11y ago
  > An algorithm which verifies "reliability" is applied to the constructed solution (e.g a proof). If this algorithm terminates then we know that we have a good solution of the original problem. If it does not then we may have to start looking for another solution. I might be misunderstanding things here, but doesn't that mean that there would exist proofs that are impossible to know the answer to, since there exist algorithms that are finite but will not terminate in human time? My brain is throwing up the Halting Problem, but I'm not entirely sure if that has any concrete relation to this.
  - Ericson2314 11y ago
    First of all, know that the Halting problem and incompleteness are very related, so you are on the right track :). Here the idea is that to type-check our proofs, if the proof language is sufficiently expressive, we need to run a program which may not terminate. But if it does terminate, we know the proof is good. From Gödel's perspective, the proof-checker is written in an inconsistent language, because infinite loops themselves prove anything! But us humans are only finite-time-patient, and we have Ctrl-C, so such technicalities are irrelevant :)
unconed 11y ago
All the code is open source, under a do-what-you-want license, including the slides, and the bulk of it is the MathBox library, designed to do exactly this sort of thing. You are free to build upon it. If this isn't considered "accessible/shareable/tweakeable" it's because the web has regressed into a bunch of walled gardens that only serve up text and media. What isn't available is a nice visual editor or a hosting platform, but that gets us into the old code vs clicking dichotomy. I don't think I'm the right person to address that, I'm far too comfortable writing code. If I make an editor, it'll still end up a tool meant to save people like me time.

Ericson2314 11y ago

Let the field medalist speak. http://www.math.ias.edu/vladimir/files/2010_09_25_slides.pdf http://www.math.ias.edu/vladimir/files/2010_09_25_slides.pdf https://www.math.ias.edu/vladimir/sites/math.ias.edu.vladimir/files/2014_08_ASC_lecture.pdf https://www.math.ias.edu/vladimir/sites/math.ias.edu.vladimi...

vinchuco 11y ago
Disregarding speech would be terrible, wouldn't it? Thanks for the pointers.
fao_ 11y ago
> An algorithm which verifies "reliability" is applied to the constructed solution (e.g a proof). If this algorithm terminates then we know that we have a good solution of the original problem. If it does not then we may have to start looking for another solution. I might be misunderstanding things here, but doesn't that mean that there would exist proofs that are impossible to know the answer to, since there exist algorithms that are finite but will not terminate in human time? My brain is throwing up the Halting Problem, but I'm not entirely sure if that has any concrete relation to this.
- Ericson2314 11y ago
  First of all, know that the Halting problem and incompleteness are very related, so you are on the right track :). Here the idea is that to type-check our proofs, if the proof language is sufficiently expressive, we need to run a program which may not terminate. But if it does terminate, we know the proof is good. From Gödel's perspective, the proof-checker is written in an inconsistent language, because infinite loops themselves prove anything! But us humans are only finite-time-patient, and we have Ctrl-C, so such technicalities are irrelevant :)

unconed 11y ago

All the code is open source, under a do-what-you-want license, including the slides, and the bulk of it is the MathBox library, designed to do exactly this sort of thing. You are free to build upon it. If this isn't considered "accessible/shareable/tweakeable" it's because the web has regressed into a bunch of walled gardens that only serve up text and media. What isn't available is a nice visual editor or a hosting platform, but that gets us into the old code vs clicking dichotomy. I don't think I'm the right person to address that, I'm far too comfortable writing code. If I make an editor, it'll still end up a tool meant to save people like me time.