So, is that basically the Taj Mahal of counter examples?

Funny that the rumour about the big Anthropic announcement had nothing to do with Navier-Stokes. It was about the formalisation of Fermat.

That was Anthropic.

Maybe society has the wrong values. Maybe society needs to rethink incentives. Maybe society is somewhat antisocial.

yes society has let the trillion dollar company down

You can say that American society made OpenAI and Anthropic possible. No other current society would have. Suddenly, formalisation of math is becoming cheap. That's not a problem, that's the goal, and it is here much earlier than expected. That's not antisocial. That is scientific progress.

(I swear, did not use an LLM for this)

You're stating it's not a problem- but I'm giving you a reason why it is. This is serendipitously mirrored by a recent post from Terence Tao on Mastodon (https://mathstodon.xyz/@tao/117207856734787448)

In most cases in pure mathematics, the problems are posed not because we desperately want the solution to these problems in and of themselves, but because we have seen from past experience that human-directed efforts to solve these problems tend to spur further development of the field through the efforts to solve such problems, and then to digest any partial or complete solutions that emerge for further insights. Prematurely solving the problem by purely AI-powered methods - particularly without full transparency into the solution process - can contaminate this process to the point where it actually becomes a net negative for the progress of mathematics as a whole.

Yes. But that is a problem for pure mathematics, not for society. I think that pure mathematics is over. At the same time, applied mathematics will probably subsume most of pure mathematics. Fermat's theorem now is applied mathematics! It will be used to improve implementations of proof assistants for a long time.

Yes, it has been. And in the form of applied mathematics it will continue to be. It is not so much that pure mathematics disappears, but that in the future there will be just mathematics, and of course it is applied. You would be surprised what kind of mathematics appears when you actually try to formalise your applications properly. It pretty much includes everything that is thought of as pure mathematics today, and much more.

Kevin Buzzard is a mathematician as well, and he thinks it's ok. I am a mathematician, too, and I know it is ok. What I find fascinating is how little mathematicians still know about this. But I am used to that attitude towards interactive theorem proving for quite some time. The difference now: if you don't adapt, you are obsolete and done for as a mathematician.

I don't really know Lean, but I think this means, three axioms on top of their whole type theory machinery, to make it classical. The type theory machinery is the obfuscated encoding of the large set of standard axioms that they don't tell you about. For example, they can encode natural numbers using that machinery.

I hear you. :-)

I think the whole trackpad idea is stupid and unusable (like anything that needs software correction for physical layout idiocy) and I blame Apple for its prevalence. Apple could make an entirely worthless product and within 4 years everyone would have to copy it.

That's like, your opinion man.

The trackpad is a fantastic input device. I use it exclusively when on a laptop, and on a desktop I'll use both a mouse and a trackpad.

Agreed… but really only for macs. That’s where it’s beautiful.

I even use their larger external trackpad with the mini. But on work supplied machines and such I use a conventional mouse.

It’s not even because everyone else's trackpads are fucking garbage (they are). It’s that systems that aren’t macs just weren’t built around using one.

Some of the slightly-less-trashy bits of 3rd party software try to bridge the gap, but it’s not the same.

> It’s not even because everyone else's trackpads are fucking garbage (they are). It’s that systems that aren’t macs just weren’t built around using one.

Great news for users depending on accessibility

Hmm, a novel style. What determines which you use at any given time? Do you just switch back and forth at random to keep things interesting?

The mouse is better for precise pointing, and the trackpad is better for scrolling (especially horizontal), and multi-touch gestures.

Not to support the idea that good touchpad is apple’s monopoly, but I and most people I know stop having wrist pains by giving up the mouse. If we’re talking about a stupid idea that’s both inefficient and a health hazard, the mouse is it. All the other pointing devices (trackball, trackpoint, rolling mouse etc) make sense one way or another

Needing a 3rd hand for a peripheral is naturally a flawed idea. The only reason I prefer the mouse over the palm trackpad is because it can't interfere while probably still having to use it occasionally. The track point and trackball were better interfaces than both but they weren't a great platform for making Apple look innovative.

the 3rd hand wasn't event what I meant by inefficient, it more that you need an extra surface to move some pointer and do the least possible amount of HCI data transfer. It's so... lame in this age of mobiliy

Yea, moving the burden from your wrists to your finger joints is surely a genius idea and the epitome of health

It would be an adequate argument if such finger pain existed

I'm not sure about the overall argument.. But I think arthritis of the fingers manifests eventually for most people who work with their hands and finger movement combined with any compression on tendons exacerbates carpal tunnel syndrome. Ergonomic I/O makers are essentially experimenting on the population, but less ethically as their bias is in using a bunch of nonsense to further a dialogue that supports whichever patents they obtained.

Personally I don't believe anything requiring 3 hands could be adequately tested given the freedom of movement given to the subject. I think only 2 hand home row keyboard use with specific additional positioning requirements has a flake of scientific rigour. (This is why I could only honestly support the track pointer in the home row as the least risky of the choices as it is the smallest deviation from something with a foundation.)

you guys are talking about a trackpad.

That is not a silly point at all. You confuse understanding the mechanics of it with having a theory of why it works. For the physics simulation, physics provides us with the theories which give us the equations underlying the physics simulation. For neural networks, why is next word prediction giving us AI that can do math? We don't really know!

There is no "theory" of tomorrow's weather. We understand the math of every single individual equation of an LLM (for example), just like we understand every single equation in the physics simulation. It's the entirety of the system that we don't understand (and hence can't predict) in our heads.

From a biology perspective - we have a good understanding of the carbon atom and how forces influence it. We really don't know much about a cell.

Usually, if you don't understand something in what an AI writes, it is a clear sign that there is a problem hidden somewhere in there. I explicitly always ask wtf exactly it means by something I don't understand, and for sure there is a problem there. AI is pretty good at isolating a problem, giving it a cute name, declaring it solved modulo cute name, and moving on.