That's a little dismissive on the series of posts, as many aren't hand-wringing. The heart of the posts including this one is about recognizing that the math community/academia needs to be better than it has been. (Rewarding teaching more over research, rewarding motivated explanations over proofs etc.)
I agree that human society is too focused on productivity but disagree that it's tied to ignorance of the Bible. The fall of man illustrated in Genesis is tied to feeding on the fruit of the tree of the knowledge of good and evil. Having the right set of religious concepts wont put you in harmony with God and thus won't make you more loving to your fellow man.
If you cannot tell a story why humans are more valuable than machines or animals, then you will begin to treat humans like machines and animals, or treat machines and animals like humans.
There are many modern examples leading to disastrous results.
Let's see how long (if it ever happens) it takes for models to generate motivated explanations (possibly done via the Manim library or something like it) along with their Lean proofs. Grant Sanderson is right that this is kind of subjective but so is Art and I'm very enthusiastic about AI generated Art.
> possibly done via the Manim library or something like it
It can be done already: the point is that the motivation and explanation parts are terrible, especially for novel topics where the AI can't just rip off existing content. A Lean proof is at least a verifiable task; you end up with an actual proof that you can work through. A Manim slop video doesn't have that.
The more I see these posts about mathematics institutions reforms and challenges from AI advancements the more it looks like they may need to go through a death. Or to put it another way they may need to start again from first principles.
If math is truly about spreading intuition and understanding then our institutions have dropped the ball decades ago and have not been able to grab hold of it since (if they ever had it to begin with)
Not sure why you're down the bottom when the current top post says pretty much the same thing. I agree that the reevaluation and refocusing that is being forced by AI is one the maths establishment could fruitfully have had a long time ago.
I'm always looking for new gui code editors. For me right now Vscode is still the top (and since I've been trying Lean out it's required). Zed is a very close second.
One thing I would like to see on the home page is a video showing it being used. Also would like to see how it looks in a light theme. The repository says it's keyboard driven does that mean it's modal or can I still use it like a normal modeless editor?
> One thing I would like to see on the home page is a video showing it being used.
Fair point. I've been meaning to record a video for a while, but I hate being in front of a camera.
> Also would like to see how it looks in a light theme.
Not great. I prefer dark themes so I haven't spent enough time making it look good on a light theme.
> The repository says it's keyboard driven does that mean it's modal or can I still use it like a normal modeless editor?
There's three modes, vim, emacs and standard, which determine the key bindings not just when opening a file, but also everywhere else. https://docs.rune.build/learn/standard-editor
Thanks. A video of the editor itself is more what I'm thinking of. Something to show how it looks to work with it and explain what itch it's scratching etc.
Interestingly that's the one point of the article I have a disagreement with. Yeah, good thinking comes when reformulating your ideas. Also, reformulating ideas is part of the traditional writing process. However it's does not necessarily focus writers/thinkers on the reformulating ideas in their most value adding form.
I've watched some YouTube videos narrated by AI that were created by those who's native language I assume to be Chinese but the value of the content is higher and more concentrated than those from the native speakers.
While I've watched many for whom English is not their first language struggle in technical talks and lose most of the meat if their discussion to their struggle with the language conversion.
While the example of language barriers being skipped over and providing value in that circumstance is obvious I suspect more is possible by avoiding unnecessarily focus on prose or technical aspects of communication and focusing on the ideas themselves.
Imagine if the cost of not assuming a background in technical/textbook writing were zero. Freeing up authors to explain more thoroughly. Perhaps, more effort can be spent on thinking up analogies, metaphor or examples to help communicate an idea.
I think this game is a better intro to lean than the Lean for Functional Programming book. However I've gotten stumped on some of the puzzles and had to Google some solutions for them since some tactics and semantics weren't explained well enough that I could intuit how to use them. And naturally, I would avoid their use until they are crucial to finishing a level (at which point I needed Gemini would point them out to me). Unfortunately, some levels even Gemini can't help with because it was trained on older versions of the game.
Reading this makes me wish someone would really try to make Project Xanadu a reality. A network built on Content Addressable Storage and a Version Control System is some thing I'd really like to see invested in.
The spec was kept proprietary and patented until about 2019. All you had before that was ramblings by an eccentric character who was 100% sure he was correct.
> Bottom crums in the granfilade represent atoms. Atoms come in two varieties: characters and orgls. Character bottom crums are stored as spans of characters, rather than individual bytes. These consist of a pointer to a block of physical storage, either in core or on disk, containing the bytes themselves, and an (integer) length, telling the number of bytes in the block. Since each of these bytes has an implicit wid of 0.0.0.0.1, the character span has a wid of 0.0.0.0.〈number of characters in the span〉. Orgl bottom crums are stored in a similar fashion, but instead of literal data bytes, pointers to the fulcrums of orgls (poomfilades) are stored.
Was this jargon normal in 1984 because we hadn't invented words like "addresses" and "structs" yet?
It's not a reality for a lack of trying. Multiple people have spent (literal!) lifetimes working on Xanadu and multiple businesses poured a great deal of money and effort into it way back in the day.
It continues to not be a thing because, even though the idea is superficially appealing to a certain engineer mind and that's why people get sucked into the cult, in reality it's not something anybody wants and it's solving a problem nobody has.
Right. I knew those people back when Autodesk owned Xanadu. The fundamental problem was that tracking and paying for text ownership and viewing down to the word level isn't really very useful. The Xanadu people were libertarians into micropayments. Everything is pay per view in Xanadu. Not cheap views, expensive ones, like Lexis/Nexis.
Also, they had no idea how to deal with either images or distributed systems.
A complex system cannot be "made" to work. It either works or it does not.
A simple system, designed from scratch, sometimes works.
Some complex systems actually work.
A complex system that works is invariably found to have evolved from a simple system that works.
A complex system designed from scratch never works and cannot be patched up to make it work. One has to start over, beginning with a working simple system. https://en.wikipedia.org/wiki/Systemantics
> Also, they had no idea how to deal with either images or distributed systems.
What would make images harder than anything else? My naive self thinks, "hey, isn't that just one long base64-encoded word?" Apparently not, or they would've done it and moved on.
And why do you say that about distributed systems? What I've read of Xanadu (primarily the Wired article) made it sound like there'd be a relatively small number of commercial servers everyone else would subscribe to. Cue IBM's "five computers are enough" apocrypha. Is that what you mean?
I find everything about Xanadu fascinating, in kind of a slow-moving train crash sort of way, and would love hearing more bystander takes!
> What would make images harder than anything else?
Because diffs of image files are not very useful. Nelson's thing was very fine-grained tracking of who wrote what. That doesn't map well to images or video.
I just finished writing a long rant on the other Project Xanadu related submission today where I specifically noted that Xanadu has a feature called a "permascroll" where everything you publish gets written into the permascroll and then transcluded into actual documents. This is a very "video editor" concept. Actually, the Xanadu model of transclusions and history would translate extremely well into nonlinear video editing; it's arguably better for video than it is for text.
Images wouldn't work unless you made a "Xanalogical image editor" that stores a list of edits and references to source images as you made or imported them. The tumbler number structure would have to be extended to include rectangular references into image files. It would work in theory, but in practice would probably bog down every computer that needed to load an image, and you'd get hit with shittons of fees for each one.
I can only imagine audio having to be stored as some kind of standardized DAW project file, with transcluded sample packs that would get you micro-transactioned for each one.
Huh, that 2nd to last article almost sounds like Amiga mod files. You pieced together samples, often, um, “borrowed” from other mods, into song-specific selection, then included a list of which samples to trigger at which frequency at which time. For example, you’d include one bass drum and one snare drum, and instructions on how to arrange them into rhythms.
Xanadu as a DAW might look a lot like that, except with explicit and documented reuse of another person’s samples.
Check out IPLD (the model that powers IPFS), which translates hash-linked DAGs and handles merkle DAGs (git) natively. There's been several attempts to build Xanadu'ish things on various types of networks, web2, web3, p2p, etc, but it just doesn't seem to be what the majority wants. Maybe someday...
I really enjoyed this video (watched it the other day). It makes me feel like it's possible for me to understand the math that I'm currently trying to understand.
I agree that human society is too focused on productivity but disagree that it's tied to ignorance of the Bible. The fall of man illustrated in Genesis is tied to feeding on the fruit of the tree of the knowledge of good and evil. Having the right set of religious concepts wont put you in harmony with God and thus won't make you more loving to your fellow man.
reply