I have proven quite a few theorems in Lean (and other provers) in my life, and the unfortunate reality is that for any non-trivial math, I still have to figure out the proof on paper first, and can only then write it in Lean. When I try to figure out the proof in Lean, I always get bogged down in details and loose sight of the bigger picture. Maybe better tactics will help. I'm not sure.
If anyone is curious about the phenomenon, the second problem in session 7 at https://incredible.pm/ [ ∀x.(r(x)→⊥)→r(f(x)) ⟹ ∃x.r(x)∧r(f(f(x))) ] is one where the proof is straightforward, but you're unlikely to get to it by just fooling around in the prover.
In principle, LLMs can do this already. If you ask Claude to express this in simple words, you will get this translation of the theorem:
"If applying f to things makes them red whenever they're not already red, then there must exist something that is red AND stays red after applying f twice to it."
Now the proof is easy to see, because it is the first thing you would try, and it works: If you have a red thing x, then either x and f(f(x)) are both red, or f(x) and f(f(f(x)) are both red. If x is not red, then f(x) is red. Qed.
You will be able to interact like this, instead of using tactics.
You don't know. Even with the best theorem provers, your definitions are still trusted. The best way I've found to help with this is to keep your definitions simple, and try to use them to do things (e.g. can you use your definition to solve other problems, does it work on some concrete examples, etc).
I think a big problem is just how US suburbs are built. Growing up in Germany, there were sidewalks, protected crossings, and public transportation everywhere, so I was just always expected to go to school and visit my friends on my own. Now that I live in the US, it's often hard to let your kids roam free, because there is a real danger of them being hit by a car.
He seems to say that the fractional reserve system is the only way society can work. But is that actually true? Quite a few banks (e.g. Brex) now allow you to keep your money in a money market fund, which invests in short term US treasuries that are protected by the full faith and credit of the US government. Importantly, in this setup, you own all the assets and the bank just acts as a custodian. And you tend to get better interest. That just seems so much saner than the bank being allowed to invest your money in risky and illiquid assets, and then we just hope that those investments don't lose too much money, or that a lot of people don't want to withdraw their money all at once.
It's the only way to keep society working. Most of the money that exists today (over 90%) is actually bank IOUs kept in their database and is what people see when they log on into their accounts.
Without a fractional reserve system, the liquidity that drives all economic activity grinds to a halt as everyone fights over the few remaining real dollars rather than managing their deployed capital.
Banks basically act to multiply the amount of money in the world today by creating promises about the future that act as a bridge that moves money from the future into the present. That money then flows into restaurants, dog walkers, software engineers, etc... Inflation is kept in check b/c the promises force the money to be paid back to the bank via monthly loan repayments.
Banks that only hold short term reserves or cash equivalents like Brex don't act as this multiplier. Going forward it's likely small banks will move towards this model as only the big banks that are too big to fail (b/c they are necessary as multipliers) can afford to take on the risk of longer term investments or creating loans.
A traditional bank used to take people's deposits and loan them to other for a fee. the fee would then be returned on aggregate to depositors less the cost of business and profit. this is so called fractional reserve banking.
But that doesn't really provide that much interest to depositors, in this age of loose money supply.
So there are more exotic functions that "investment" banks fiddle with. Ie trading on the stock market (regulated betting) buying companies, and trading on futures and other pure bets.
The problem is that banks are bigger, and have more depositors. So when one pops, other go because they are all doing the same shady shit to make profit.
In the UK there are still a few building societies that offer traditional, boring, consumer banking and mortgages. But they are now large national behemoths.
But to your point, Brex is a payment manager/facilitator. Its not really offering banking, its more a service to manage expenditure. This might seem like pedantry, but its different enough to make the point.
I would disagree that Brex (and many others in the space) aren't offering banking. I can deposit money, I can withdraw it, I have a credit card, I earn interest, etc, they seem to offer everything a traditional bank would.
To your point about risky investments, like stocks, I agree that that's very sketchy. But I think even very prudent banks that don't invest in stocks etc still take on a lot of risk, like we see with the bank collapses caused by the high interest rates these days.
Having 4 kids ages 5 and under, while also running a startup, I can confidently tell you that disposable dishes are the true answer to efficient dishwasher management.
That seems a little strong. We spend like $50/month on paper plates, which are compostable, and I get back many hours of my life that I can use to create valuable experiences with my kids. I don't think that's anymore morally wrong, then say, going on a vacation.
This actually became a political issue in Israel- ultra orthodox Jews could easily have more than 4 kids ages 5 and under while their religion forbids them from washing dishes or use electrical appliances on Shabbat (Friday evening-Saturday) so they tend to buy disposable dishes being in conflict with a country trying to be somewhat green.
In 2013, it seemed that Google intended to expanding its online search dominance into the real world by cataloguing books, and then giving users access to the contents of books in search results.
They did some of that, but it didn't pan out as successfully as was imagined.
I'd be curious to. Wikipedia seems to says that this might be mostly marketing speak. 'The term "3 nanometer" has no relation to any actual physical feature (such as gate length, metal pitch or gate pitch) of the transistors. According to the projections contained in the 2021 update of the International Roadmap for Devices and Systems published by IEEE Standards Association Industry Connection, a 3 nm node is expected to have a contacted gate pitch of 48 nanometers and a tightest metal pitch of 24 nanometers.'
Thanks for the thorough writeup! I agree that our implementation seems to solve your use-case.
Let me provide you with a bit more context about the house buying use case. When buying houses you need to keep a chunk of money (around $60k) available to wire next day for a "good faith deposit" in case you're the winning bid, and it's quite a waste to keep that money in a checking or savings account (since the house buying process can take months).
Since Financial Choice only allows 50% accessible in Instant Access, in your home buying example I would need to have $120K in my account to make a $60K transfer (ignoring the possibility of a market downturn). Is a long term goal of Financial Choice for users to treat this less like a checking account where you hold cash for near term spending and more like a one-stop shop where all your assets are held?
Great question. The motivation will differ from person to person, but I can give you the reason why I'm using it.
I live in a high cost of living area, so I used to keep ~20K in my checking account at all times to pay for rent etc. All the rest of my money I invested in a total market stock index fund. The checking account balance is just a small fraction of my overall balance, so the FDIC insurance really didn't help me.
Financial Choice has two benefits for me. 1) I now get to invest those ~20K which gives me a ~1-2K expected annual return without any hassle, and 2) I can just keep all my money in my Financial Choice account, so I don't need to bother moving money between a checking and brokerage account anymore.
Good question. Here's the difference. When you withdraw money from Charles Schwab and there's no cash in your account, it creates a margin debt. You then have to pay that margin debt back manually, and you pay interest until you do. With Financial Choice, we automatically sell your investments to cover your withdraws so you don't build up that margin debt.
> With Financial Choice, we automatically sell your investments to cover your withdraws so you don't build up that margin debt.
If I withdraw $10,000 with that Charles Schwab margin debt, and let's say I repay it 3 months later, how much interest will I have paid to Charles Schwab? (Napkin calculation, I'm not quite sure what the interest rates is on those margin debt.)
With your product, indeed no margin debt, but if those 10k are obtained from an investment were originally a 5k investment from many years ago, then, assuming 20% ltcg + niit, I suddenly owe around $1200 to the IRS, and some other $$$ to the state maybe.
In which situations do you see this being a better money move than the margin debt way?
2 additional questions :
- when selling do you minimize tax (i.e. attempt to sell the lot with the least amount of gain)
- do you attempt to "cover" taxes? (i.e. withdraw actually ~$12k, so that i roughly have $10k actual cash, and the rest to pay the IRS bills - assuming your users can indicate which marginal tax bracket they fall in after W2s)
I'm probably not your target customer but I see having to manually rebalance my portfolio as a feature not a bug.
I would be very interested if you could find a way to provide me with a short term(net 30 days) low cost(<2%) margin loan. I wouldn't even really mind giving up some price execution (i.e payment for order flow) so you can make money.
reply