Hacker News Reader

Hacker News

Comment by raverbashing | Hacker News Reader

Parent Full thread

raverbashing

Not really

A proof that works is the most important part. After that you can make it nice

View on HN

> you can make it nice

Not the 200 terabyte one, you can't.

Maybe we can use the brute force of a "math superoptimizer" to "compress" it to something far more reasonable. If we teach said opimizer what structures are well understood by humans we might actually understand at last parts.

I don't know why people keep thinking there's something special about the way we humans do calculations vs what could be achieved with a complex enough computer

These are not mere calculations. See, an understandable proof has more structure than plain first order logic alone. This allows such proofs to be extended and worked upon as well as real life implications to be discovered.

Math is not about proofing something, or creating a as big as possible collection of lemmas. Math is about creating structures that can use as tools to solve problems. And problem solving is a task done by humans, so math is only useful if humans understand it and have a intuition.

I have a couple of experiences of doing similar big projects where we counted the number of some objects (I haven't checked how big they are.. I have run SAT solvers for a couple of weeks, I didn't try to record some "proof size", I imagine it would be as big if not bigger than 200 terabytes).

Once I could tell a mathematician the count, in both cases someone they proved the result in an alternative way fairly soon afterwards :)

It never occurred to me until just now that one of the AI overlord scenarios, and also quite possibly the most plausible one, is one in which AI just exploits some impenetrable proofs to win at economics via information asymmetry. Rather than rounding us up or exterminating us, we just become the live at home kid always begging for money, grumbling about a curfew and having to do chores at 25.

This scenario can be boycotted as long as humanity owns some land and capital and boycott all AI overlord services.

I think that's basically the plot of Asimov's The Life and Times of Multivac

Reply on news.ycombinator.com