bobajeff

From the outside seeing academics wash over concerns and debates about this it's helped me sort of get more comfortable with around my own questions about what I want from math and computers. What I've come to realize it's that I just want tools that do a job and enjoy learning them. I also get gratification of being creative with them. I'm not in it for expanding human knowledge or seeing the beauty in the universe or the pleasure of understanding something difficult.

That sounds very simple. And yet it's apparently not:

https://github.com/bevyengine/bevy/issues/26055

Unfortunately, Wayland is a default feature in bevy and the only way to not include is too disable default features and manually enable the features you need which requires a very deep understand if the project (which so far I've not found anyone who fits that description)

No just without Wayland. My system didn't have Wayland installed because it's old enough not to include it by default and my card doesn't support it. However, a short while ago I got it to build by installing libwayland. (I was afraid my system might break by installing it but that doesn't seem to be the case so far.)

Yeah I was wondering if some things are more coupled together. The issue I'm having is building it on a system without Wayland installed is very hard (or possibly impossible).

By some coincidence I've been looking at bevy and other engines lately. Bevy sounds like it had thought put into it's library to make it more modular. However so far it very hard to even get started in it. (Haven't even gotten it to build)

I think that's ultimately a good thing. As proofs weren't supposed to be the point as stated by William Thurston long ago. Maybe now the focus can be more on better explanations and creating tools for growing understanding and intuition.

Awesome, I love it. I never even heard of the Vectrex before. I'm guessing it was too expensive for most people since it's basically a whole arcade machine.

Is not just games. I've already seen the beginnings of proprietary software such as Wolfram Engine and Microsoft Word vibed up into alternatives. How long till all of MS Office, Creative Cloud, Houdini get the same treatment? Truly exciting times.

I like the concept and these explainers. It sounds like this is using a HTML based format to be similar to like a Flash / Shockwave animation to keep data size down.

I wonder what the challenge would be of making these videos more interactive would be? Also I do wonder if there is any research happening in making AI explainers more trustable.

That doesn't follow. I'm not especially gifted at mental math yet I've been able to learn various programming languages and libraries and dev tools. I've also been able understand and implement some algorithms.

Why not just use the calculator app on your smart phone? That's what I do. (School made me all too aware of how easy it is for me to get the wrong answer when trying to do calculations mentally)

As sometime who's memorized but also forgotten their timetables while still managing to go through Algebra I. I don't understand the importance for memorizing times tables (or any other tables for that matter).

I for one cannot be convinced that these companies saying they want to slow down AI progress is for the safety of mankind (or any other altruistic reason). However, I respect someone willing to give up a very comfortable career for his convictions.

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.

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.

Interesting, looks like this is a framework built on Flutter.

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)

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.

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?

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.