ogogmad

> correlated to

Correlation measures whether Y=mX+c holds with small error. I sometimes think that many people unknowingly assume that all dependencies are somehow straight-line ones. This is distinct however from "linear approximations" in physics, which can at least be justified sometimes.

I also suspect that correlations of 0.5 or lower are often just statistical noise.

In my experience they write an informal proof first, check it without Lean, and only then turn it into Lean code. That last step sometimes takes them much longer than checking their proof without Lean, which is a problem humans have as well. What they're truly bad at, however, is explaining their proofs. Until they improve at that, we'll have to keep resorting to Lean to check whether they solved something correctly.

I'm less sure about the following, however: I think that while current LLMs are bad at explaining their own proofs, some models are great for discussing older, human-written proofs. For this use case, from best to worst, Gemini > Claude > GPT-Astra >>>>>>>>>>>> GPT-Sol.

That's not what "attention" means.

> it’s not going to create novel insight beyond the arguments made from compressed snapshots of existing knowledge

So all of the maths breakthroughs were not novel?

Wondering how that compares to dependent types.

I personally think that Pratt is a combination of recursive descent and precedence-climbing. Maybe even the combination? Those ideas are individually older than Pratt.

"Pratt can't parse statements" - can't you treat ';' as an operator whose meaning is "then"? You can then read "DOTHIS(); DOTHAT()" as an expression.

How are people finding Fil-C? It's designed to avoid things like this.

What if people become increasingly dependent on their government’s spending beyond its means - so that they suffer more harm once the deficit is reduced than had it never been raised in the first place - making it impossible to rein in the deficit when borrowing costs rise and the debt is high?

They are controversial because supporting them raises matching time to O(2^n) in the worst case - which is dangerous - while not supporting them enables matching time to be O(n) in the worst case. And a user might not be aware of that danger.

Also, I think it's misleading to mention NFAs and DFAs alone, like there's no deeper reason. The deeper reason is that:

  Regexes (or NFAs, or DFAs) classify exactly the properties of strings which can be checked in constant space.

It turns out that any such string property can also be checked in O(n) time, and in one single left-to-right pass.

Briefly returning to backreferences, supporting them makes constant space unachievable. They also make linear time unachievable, since matching them becomes NP-COMPLETE.

Also, no regex implementation actually uses DFAs. NFAs yes, but DFAs no. The point of NFAs is that they're easy to execute in constant space and linear time, while also making concatenation and Kleene star easy to implement. It seems much harder to implement concatenation and Kleene star using most other constant-space automata - like DFAs - which is what actually forced people to invent NFAs.

I think some languages do have a library-style version of regex. But the function names aren't consistent between the different libraries. Maybe then we need to put on special goggles to make them look the same.

Backreferencing inside of a regex (which is a way to find repeat occurrences of a substring) is a very controversial feature that some regex engines intentionally omit, while most others support it only grudgingly. Supporting backreferences opens up a big can of worms: Most regex engines will fall back to a slow, poorly optimised algorithm if they ever encounter backreferences.

Also, it's important for people not to confuse backreferences with capture groups. They look a bit similar, but capture groups are actually fine.

In fact, backreferencing is such a footgun that I don't see it as a possible regex feature. It's a PCRE feature - perhaps even the core distinguishing feature. While all regexes are PCREs, not all PCREs are regexes. It's simply not possible to create a consistently performant implementation of PCRE.

Autodidact here. Beyond just the five core quantifiers

  .
  |
  ?
  *
  +

regex only has capture groups

  ()

and lazy variants of the core quantifiers "?", "*" and "+", which are helpfully called:

  ??
  *?
  +?

The rest is just shorthands.

So while I think it's a worthwhile suggestion not to show people the whole thing the first time round, I doubt that the whole thing is really that complicated.

Really cool. Do you teach people the mechanics, like what the app shows? Because I wonder if that actually makes it harder. I'm wondering about where the hard bits are, given that it all boils down to just:

  "|", which means "or"
  ".", which means "any symbol"
  "?", which means "at most once",
  "*", which means "however many times"
  "+", which means "at least once"

Maybe encountering it next to PEG scrambles your brain.

It's code golf played with Turing machines. The game is: Make the smallest Turing machine whose runtime is bigger than Graham's number, but still terminates. The record right now is 10 states. At least 6 states are needed because any Turing machine with at most 5 states, that finishes running, has a runtime of at most 47,176,870, which is less than Graham's number. In summary:

  BB(10) > G > BB(5) = 47,176,870.

Dijkstra's jeremiads were about promoting "formal methods" as the One True Method for software construction. Maybe there's a future for formal methods, but it wasn't ready in the past. No one was arguing about semaphores.

Dijkstra was an academic with no skin in the game.

If Dijkstra was so confident that he was right, he should have started a business and put his money where his mouth was. Hell, any True Believer of Dijkstra's could have done the same in the last 60 years. The fact that they haven't - or they've never succeeded enough for me to know of any - speaks volumes about their effectiveness.

The constants can be made lower. If we didn't know about the galactic algorithm beforehand, we couldn't begin to do that.

A lot of people have been surprised by the interest that AI companies have in solving maths problems without obvious applications, as well as in the financially precarious state of these companies. I imagine that they thought that these companies were helmed by mere bean-counters, like at Boeing. But no, I reckon that they're still academics at heart, and so they work on Navier-Stokes and L=BPL, instead of on how to maximise value for their (soon to be) shareholders.

  Don't hire a straight-A student, unless it's to take exams; or a professor, unless it's to write papers.
 -- Nassim Taleb

How interesting that Anthropic and OpenAI are full of professors and straight-A students!

Who decreed that they are entitled to get paid for that?

Maybe this hurts more than it should do because of publish-or-perish.

>> virtually none of this stuff is possible with technology any normal citizen has access to.

Initially, yes. Long term, however? Perhaps still yes.

> 5) professors are left to rewrite the AI Lean slop into real human-readable math?

6) AI writes the proof into something easier to follow than a PDF document.

Hmm. Oh shit.

> The risk here is that this does do fundamental long-term damage to mathematics as a viable field.

All the commotion evens out: It's much easier to learn maths than ever before; you don't need to go to lectures any more; you don't need to learn from a specialist (advisor, lecturer) any more; it all costs much less than it used to.

So mathematics will continue to advance, albeit differently from before. The social structures will not survive however.

Is this not greed?

Yes today but maybe no tomorrow.

What if merging with them doesn't make them better at anything, but worse? Would that be a concern?

You're a Nazi piece of shit. [edit: removed identifying information]

Supposedly autistic, therefore loser? You're hideous. You fuck off.

This reaches 1/3 milestones deemed a "breakthrough" by Epoch AI: https://epoch.ai/frontiermath/open-problems/apery-irrational...

The remaining two "breakthrough" milestones are (i) a proof or refutation of the Poincaré conjecture in 4 dimensions (ii) an improvement to the best-known classical prime factorisation algorithms.

> AIs are outright terrible explainers

Gemini's explanations are very good.

The problem with what you're saying is that any old random true proposition about the integers is not necessarily interesting enough to be called a theorem. GIT (or the uncomputability of the Busy Beaver problem) does not establish a limitation on proving theorems, but rather on determining whether a proposition is true or not. Most propositions are ugly and irrelevant. So GIT/Busy Beaver is irrelevant.

-----

Oh, and: All proofs are conditional on axioms. If those axioms are computably enumerable, then all of their consequences are computably enumerable too.