As a follow-up: I did this for a while, but I’ve become convinced there are a couple effects that make this not as good as it sounds:

Futures have taxes paid in the year gains are made, which significantly reduces returns in simulations I’ve run. In an ETF or mutual fund, you can instead let those gains ride.

Futures have an implicit financing cost, and portfolio performance is very sensitive to this cost if you’re using a lot of leverage (e.g. for intermediate term bonds).

Leveraged ETFs fluctuate a lot, and need to be rebalanced with the rest of your portfolio. This causes taxes like above. If you don’t rebalance, your leverage ratio changes which causes the portfolio to behave poorly as well.

With all of these effects accounted for, the gains from leveraging look very modest and depend a lot on what time period you look at. Given the risks, I’ve decided against it for myself.

For those who are:

Mathematically literate, but

Not familiar with this particular analogy (of proofs <-> agents)

Do you know of a good reference for how to interpret discussions like this?

For example: ”A tries to prove that A→B, and B tries to prove A”—If A and B are propositions, what does it mean for a proposition to try and prove another proposition?

(There might be more language that needs interpreting, but I got stuck there.)