viscousviolin

Bobbybroccoli over on Youtube made three massive episodes about the story that goes into it with a lot of detail - I couldn't stop watching them when I first found them. Here's the link if anyone is interested: https://www.youtube.com/playlist?list=PLAB-wWbHL7Vsfl4PoQpNs...

Thirty days of preventive detention is outrageous. Way to go Bavaria.

Does anyone feel like trying this out with some folks from here?

It's easy on the eyes and it can make reading lots of equations less awkward if done correctly. I remember finding out this was possible while I was working on an assignment in Latex - it looked amazing.

It takes a little bit of work to colour in equations but I hope more people start doing it (including me, I'd forgotten about it for a while)

That's not my point. In the comment I made below the other post I talked about how Mathlib is just a piece of the puzzle, the way I see it [0]. I don't want to see Lean do symbolic computation - although I'm sure that would be great as well - what I want to see is to have Mathlib's library of mathematics being used in a way that any CAS can read definitions and theorems from it. Then a significant part of the CAS codebase won't have to be manually written, and developers can spend time on things that are not re-inventing some wheel.

[0] https://news.ycombinator.com/item?id=37435449

How about Lean? [0] There's a whole library of mathematics written down in Lean called Mathlib, which spans most of the undergraduate maths curriculum upto some cutting edge research-level maths. I've commented under the Part II post you linked to as well, describing how I think Mathlib could help the CAS ecosystem.

[0] https://leanprover-community.github.io/

I don't think it's as difficult as you think it is. It's still a lot of work to implement mind you, but not nearly impossible. I talked about Mathlib [0] in a reply to the grandparent comment, which is a library of mathematical theorems and proofs that has a big community effort behind it. The language they use to state theorems would help a lot in making mathematics machine-readable enough for a computer algebra system to be able to make sense of it.

I'm hoping to build a prototype for this sometime in Julia's `Symbolics.jl` CAS. It would be just a simple proof of concept to implement derivative and integral rules from Mathlib or some custom maths library, and get them into the CAS. Symbolics.jl seems to be a perfect fit for this since it's made to be extensible, and Julia's metaprogramming would be a welcome addition as well. Either way, I would love to see this become part of the CAS ecosystem.

[0] https://leanprover-community.github.io/

It's been on my mind lately as well. I was trying out `symbolics.jl` (a CAS written in Julia), and it turned out that it didn't support symbolic integration beyond simple linear functions or polynomials (at least back then, things have changed now it seems). Implementing a generic algorithm for finding integrals is hard, but I was expecting more from that CAS since this seems to be implemented in most other CASs. The thing is that every single CAS that covers general maths knowledge will have to implement the same algorithm, while it's hard to do it even once!

I feel like at least a large part of the functionality of a general purpose CAS can be written down once, and every CAS out there could benefit from it, similar to what the Language Server Protocol did for programming tools. They also had to rewrite the same tool for some language multiple times because there are lots of editors out there, and the LSP cut the time investment down a lot. They did have to invest a large amount of time to get LSP up and running, and it'll have to be maintained, but I think it's orders of magnitudes more efficient than having every tool developed and maintained for every single (programming language, editor) pair out there.

Main problem is like you said how to write down mathematical knowledge in a way that all CASs can understand it. I've been learning about Mathlib lately [0], which seems like a great starting point for this. It is as far as I know one of the first machine readable libraries of mathematical knowledge; it has a large community which has been pushing it continuously forward for years into research-level mathematics and covering the entire undergraduate maths curriculum and it's still accelerating. If some kind of protocol can be designed to read from libraries like this and turn it into CAS code, that would be a major step towards making the CAS ecosystem more sustainable I think.

It's not exactly what you were talking about, as in, this would allow multiple CASs to co-exist and benefit from each other, but I think that's better than having one massive CAS that has a monopoly. No software is perfect, but having a diverse set of choices that are open source would be more than enough to satisfy everyone.

(I have posted about this before [1] on the Lean Zulip forum. It's open to everyone to read without an account)

[0] https://leanprover-community.github.io/ [1] https://leanprover.zulipchat.com/#narrow/stream/113488-gener...

We're all tired of it.

Something that would help speed up development of new interfaces would be applications having more extensibility in general. It happens so often that I come across a piece of software where I want to change just one thing, but there's no easy way to do it with plugins or extensions. The alternative is to create the software mostly from scratch myself, which is way too much effort that's just not worth it. Imagine what would happen if you could see all those small changes stack up, we could have so much more interesting functionality.

Github's backup on Svalbard also uses some kind of film, and it's supposed to last 500 to 1000 years: https://en.m.wikipedia.org/wiki/Arctic_World_Archive

Forgetting so much is my current fear as well. What did you end up doing?

Selling data would be a bad move for sure. I can't seem to find anything when I search for it, do you maybe have a source I could take a look at?

I get that, which is exactly why you don't want any one browser having just under 70% marketshare like Chrome. If there are multiple options for people to switch between, then they can switch to another one if their current browser does something they don't agree with.

If there isn't another option, you're stuck. We open ourselves up to horrific effects of browser monopolies like all the security issues that Microsoft didn't give a damn about back when internet explorer had a monopoly. It takes effort to switch to a different browser stack, like moving away from Chromium for example, but in the long term you do not want everyone stuck with only one option, because that will be even more costly.

Ah, I see what you mean. I'm personally not against this at all, since the Firefox devs need feedback on what's working and what isn't. But I completely understand that some people won't accept this. Only thing I can't figure out is if this is opt-out or opt-in, because I might have mindlessly clicked yes on opting in during installation.

Are you talking about firefox not blocking website adds by default?

I hadn't heard about the Mr.Robot fiasco, that's seriously troubling..

Oh interesting! Seems like a pretty specific requirement to have. Do you mind if I ask what you use those for?

As for the tracking - I'm pretty sure Firefox blocks a lot of those by default, last time I checked it was plastered all across their homepage. It's not 100% effective, but if them making an effort to do the right thing pushes you away, you might be asking too much unfortunately. Building an entire browser takes a lot of energy and time, and Firefox seems like the kind of browser that's worth it in the long term.

What makes you not trust firefox? I don't remember hearing about them acting in bad faith, but I'd love to hear if they did. What features do you need that only Chromium can give you?

Yes, it's not a problem. For now. There are so many software projects that depend on chromium for their basic functionality, and so many users that indirectly rely on chromium. It's hard to switch to an alternative if the need arises. So when Google inevitably turns chromium into a problem, you don't have enough time to switch, no matter how badly you want to. It's time to preventatively switch to a project that's more reliable. Give Firefox's Gecko engine a chance, it has all the features you need. It would take a lot of effort, but we'd be protecting ourselves from a pretty realistic scenario where Google just pushes through whatever they want.

Unrelated to the outage, but I'm curious nonetheless: would it be possible to hook up Tarsnap's encryption software to a Dropbox folder? I'm not sure if it even makes sense to use Tarsnap for this, but I'd love to have an easy setup that allows me to use Dropbox's servers but only let them see encrypted data so they can't snoop.

I can't wait until e-paper tablets become mainstream and more companies start making them. Having a generic OS like Android or Linux, instead of the closed off system of a kindle or whatever, would be amazing. Imagine how many different kinds of apps you can run on something like that.

With colour e-paper screens slowly picking up speed it's going to be even more interesting. Right now their quality is going to be disappointing if you expect the same quality as your phone or laptop, but it's an enormous step up from greyscale screens - and it's still getting better.

I found a book on folding algorithms a while back. It's called "Geometric Folding Algorithms: Linkages, Origami, Polyhedra" by Demaine and O'Rourke. I haven't gone through it myself yet, but I feel like they should have an answer for you.

(They also have a really nice course on MIT's Open Courseware that covers their book: https://ocw.mit.edu/courses/6-849-geometric-folding-algorith....)

I like your four day interval - was the reason you choose this to not spam people?

Seems like this is what Matt Parker built together with some other people a few years ago: https://www.youtube.com/watch?v=R9c-_neaxeU&ab_channel=Stand.... It's incredibly inefficient compared to running it on a computer, but an amazing way to teach kids about this.