It is not so obvious, some countries have a wealth tax in addition to the income tax.

Only if you pay it off with taxable income.

If you have a lot of assets you can just refinance your loan with more debt.

This makes no sense. How is lender going to make money?

They still charge interest but at a rate lower than the tax rate of earning it as income.

Part of the Advent of Compiler Optimisations https://xania.org/AoCO2025

Loving it so far!

We used a low number _and_ it was a while ago (it would be different if we used the same number spread out on the same time span)

I find it much easier to see what is going on when selecting λ-calculus instead of Δ-Nets. E.g. for the mandatory Y Combinator,

λf.(λx.f (x x)) (λx.f (x x))

for which the difference with

λf.(λx.f (x x)) (λx.f (x x) f)

is very clear, whereas with Δ-nets the difference is more subtle. I guess it is because the visualization has more information than with the λ-calculus.

First sentence:

> All of modern mathematics is built on the foundation of set theory

That's ignoring most of formalized mathematics, which is progressing rapidly and definitely modern. Lean and Rocq for example are founded on type theory, not set theory.

I think what is more accurate to say is that the broad crisis in foundations of mathematics was initially resolved by formalizing set theory.

Not a mathematician, but AFAIK ZFC is a valid foundation. Dependent types helps a lot with bookkeeping, but cannot prove more theorems.

Lawrence Paulson is a great person to clarify those topics (Isabelle/HOL is not based on types yet it can proof most maths).

> but cannot prove more theorems

usually you're more interested in better ergonomics: can you do X with less work?

it's like picking a programming language - depending on what you're attempting, some will be more helpful.

and ZFC is a lot more low level than what day-to-day mathematics usually bothers with. So most mathematians actually work in an informally understood higher-order wrapper, hoping that what they write sufficiently explains the actual "machine code"

the idea then behind adopting alternative foundations is that these come with "batteries included" and map more directly to the domain language.

>hoping that what they write sufficiently explains the actual "machine code"

actual, having faith that what they write could compile, run, and pass tests, but never doing so.

Isabelle/HOL is still types. The underlying type theory of Isabelle/HOL is not theory of dependent types, but theory of simple types. Isabelle/ZF would be a better example as it encodes Zermelo–Fraenkel set theory.

Right!

It’s not really. It leads to paradoxes. There are alternative formulations which avoid these.

Uh? Could you write an example or two?

And formalised mathematics are ignored in mathematical practice by most mathematicians, and even the ones that know of it often don't use that as a foundational language due to relative inconvenience.

I think at this stage, most mathematicians recognize that formal proof verification is a real and interesting thing. We have extremely prominent mathematicians like Scholze & Tao making a point of using these tools.

But in many cases, it's extra effort for not much reward. The patterns which most mathemematicians are interested in are (generally) independent of the particular foundations used to realize them. Whether one invests the effort into formal verification depends on how hard the argument is and how crucial the theorem.

You are conflating two things - the language of math, and the language of proving facts about the language of math.

The former is almost entirely sets, while the later is necessarily types.

agreed.

tiring.

maybe someone will make an "article-to-prompt" sort of reverse ChatGPT?

But of course someone already did that, and of course it's inside ChatGPT, what was I thinking? Though if I do try it, the prompt I get is not especially pleasant to read: https://chatgpt.com/share/6926f33c-8f98-8011-984e-54e49fdbb0...

> Thatcher told us, “There is no alternative.” In 1982, Bill Gibson refuted her thus: “The street finds its own uses for things.” > I know which prophet I’m gonna follow.

> Thanks to a free AI model that ran on my modest laptop, in the background while I was doing other work, I was able to write [an accurate quote]

He's right, but it sure sounds like a long fight made of small actions.

I really liked the definition of reverse-centaur

> A reverse-centaur is a machine that is assisted by a human being, who is expected to work at the machine’s pace.

This exactly describes the attitude of a PM I work with who makes abundant use of ChatGPT to generate PRDs.

We get so much crap for not keeping up with the flood of requirements. "Why don't you just plug my specs into Claude Code, review it, just tell Claude what needs to be fixed?" Its exhausting.

I really do feel like a reverse-centaur. I'm genuinely expected to work at the pace of this rube goldberg bullshit machine this PM has rigged up.

But is there really an alternative?

Another one is Presburger Arithmetic, which is Peano Arithmetic minus the multiplication. What makes it interesting (and useful) is that this removal makes the theory decidable.

https://en.wikipedia.org/wiki/Presburger_arithmetic

Skolem arithmetic is decidable too: https://en.wikipedia.org/wiki/Skolem_arithmetic

I'm wondering whether there are decidable first-order theories about the natural numbers that are stronger than either Skolem or Presburger arithmetic, that presumably use more powerful number theory. Ask "Deep Research"?

[edit] Found something without AI help: The theory of real-closed fields is decidable, PLUS the theory of p-adically closed fields is also decidable - then combined with Hasse's Principle, this might take you beyond Skolem.

[edit] Speculating about something else: Is there a decidable first-order theory of some aspects of analytic number theory, like Dirichlet series? That might also take you beyond Skolem. https://en.wikipedia.org/wiki/Analytic_number_theory#Methods...

I recently learned about https://en.wikipedia.org/wiki/Self-verifying_theories which gives you most of multiplication while still being decidable, which is pretty crazy.

That's cool, but where does it say it's decidable?

Not on that Wikipedia page, but you might want to have a look at the papers?

Some decidable extensions of Skolem and Presburger, searched for and found by ChatGPT: https://chatgpt.com/share/67e1d302-c930-800f-bc2a-85bdc60563...

There are no specific extensions mentioned, a bunch of math symbol rendering issues, and what seems like maybe some hallucinations? Thanks for proving once again how useless chatgpt is if you're not already an expert on what you're asking it

> fixing the climate

I would be happy to be convinced that climate is an intelligence problem.

One could argue it could be solved with "abundant energy" but if this abundant energy comes from some new intelligence then we are probably several decades away from having it running commercially. I would also be happy to be convinced that we do have this kind of time to act for climate.