OxO4

To an extent, that is what automated theorem provers (e.g., SAT/SMT solvers) do quite successfully. The monkeys have very good heuristics and avoid going down unnecessary paths, but they are still monkeys. Similarly, AI might be very good at recognizing patterns (which is very useful!), but doesn't necessarily demonstrate any kind of real understanding.

Of course humans make mistakes, but (outside of Lean at least) they attempt to solve it with experience, understanding, and a certain amount of creativity instead of mashing things together until something works out.

Right, my comment was not about its usefulness. I was merely pointing out that those results do not necessarily imply any kind of actual understanding.

The recent progress does not imply that the "impersonator" has a deep understanding of mathematics. By formalizing a problem in Lean, constructing the proof is essentially a complex search. Because Lean is the arbitrator of correctness, the "impersonator" can make as many mistakes as they want until they find a solution that passes the checker. That is very different from checking a paper for correctness.

The Top Gear video mentions that kind of recharge time using an external system (though they do claim that they are trying to get it down to 30min).

I've seen some claims that the gas is stored at a pressure of 10000 psi/690 bar in a 200 l tank. If that's true, then that is a gas volume of 138000 l. A commercial, stationary scuba compressor compresses around 850 l/min [0] to 350 bar. A compressor like that would take around 160 min just to compress 138000 l to 350 bar (so significantly less than 690 bar), is a _large_ appliance, and _loud_. Compressing gas quickly also produces heat. An on-board compressor seems quite unrealistic to me unless I'm missing something.

[0] https://www.bauer-kompressoren.de/en_en/pe-ve1

Based on a cursory search, propellant-grade nitrogen requires a high purity (99.99%) [0]. I am no aerospace engineer, but I'd be interested to know what the actual requirements are for a system like that to work reliably. If 99.99% nitrogen is actually required, then I'd assume that the corresponding compressor would neither be compact nor particularly maintenance-free.

[0] MIL-PRF-27401

The funny thing is that during the event, Elon claimed that the car can recharge the tanks itself [0], but in the Top Gear video, the Tesla folks say that it is recharged from an external source [1]. In the Top Gear video, they also say that they are filling it from a "high pressure nitrogen system", whereas Elon claims that the tank is filled with air. They can't even keep their own messaging straight.

[0] https://www.youtube.com/live/qt5p-_tE8d0?si=V5csPghK02wwd0or...

[1] https://youtu.be/JdkIOhFmbKI?si=ULvyIRWDRZRWlIWA&t=1340

There are people that are taller than six foot and it also depends heavily on whether you have long legs or a long torso.

If you are tall, then no amount of reclining is going to give you more space. The knees are too far forward to stretch your legs, _especially_ when the person in front of you reclines.

In other words, you are inconsiderate.

Are you suggesting that you can tell the types of games someone enjoys by just looking at them?

(Your reply is another example of right-wing discourse being around prejudiced assumptions instead of reality.)

People like you sanewashing the actions of this admin are a major part of the problem.

Even if this were how the system was designed, it is time to acknowledge that it is fundamentally broken and needs change. It is mind boggling that the response to these issues amounts to WONTFIX.

FWIW, some "smarter" machines (e.g., [0, 1]) support taking three readings with a minute pause in-between and then spit out a single reading.

[0] https://www.garmin.com/en-US/p/716808/ [1] https://www.withings.com/us/en/bpm-connect

Freedivers are also taught not to exhale underwater, because it wastes oxygen and lowers your CO2 level, making it harder to know when you actually have to come back up. Your body can't sense the level of oxygen it has, so freedivers rely on CO2 levels as a proxy, so messing with it is dangerous.

> I don't think the government leadership has my best interests at heart

And for-profit companies have your best interest at heart? With government services you can at least optimize for goals other than profit.

Great. Housing should not be an investment and chasing ever-increasing property values as a society is obviously unsustainable. If you own a house as your primary residence, then its market value shouldn't really matter, because the value has no impact on your quality of life.

Often, people try justify high pay for management positions by pointing out the responsibilities that comes with such a position. If that's the case, then it only makes sense to place blame on management when things go sideways. If not, then what exactly is the value that management adds to the company that justifies their high pay?

How so? The 2023 models of the F150 seem to get about 17.19 MPG [0] which is significantly worse than the 32.34 MPG [1] of the 2023 Escape.

[0] https://www.fuelly.com/car/ford/f-150/2023

[1] https://www.fuelly.com/car/ford/escape/2023

It seems that iFixit will officially be selling replacement parts for Google's Pixel phones [0] and Valve's Steam Deck [1], so hopefully, they are not going anywhere.

[0] https://www.blog.google/outreach-initiatives/sustainability/...

[1] https://store.steampowered.com/news/app/1675180/view/4347665...

Not defending the other design choices, but there are places in snowy mountain areas where (almost) flat roofs are common [0].

[0] https://www.davos.ch/en/information/portrait-image/storybook...

Can we please stop suggesting that anti-LGBTQ "viewpoints" are worth exploring and that people are just to "embattled" on the issue of basic human decency?

There's a standard for automatically sharing the current location with emergency services, which is supported by both Android and iOS [0]. According to the wiki article, the UK is even one of the countries that uses AML.

[0] https://en.wikipedia.org/wiki/Advanced_Mobile_Location

Would your "free market" also mean that the people living in the suburbs pay the true cost of living in suburbs? Including higher taxes to offset the higher infrastructure costs and the higher impact on the environment?

FWIW, Luke Smith has some problematic political views (as in far right/alt-right). You do you but I personally avoid sharing/using any of his content for that reason.

> SAT solving is about 95+% of SMT solving

This is theory-dependent, I would say. It is certainly true for bit-vector solvers that bit-blast for example. For other theories, however, this is not necessarily the case. Consider a simplex-based linear integer arithmetic solver for example. If there is a problem that is simple at the Boolean level, you may end up spending more time in the simplex solver.

Lowering the seat will also make it quite a bit worse for people with long legs. The height of the usual seats is already too low. It would be better if they raised the middle seat instead but I guess that adds cost/weight.

They don't ship the laptop, they send a technician and do the repair on-site. I have personal experience with a Lenovo ThinkPad. Dispatching the technician may have taken one or two business days (I don't remember exactly).

That's just not true. Depending on your warranty you could have on-site service. In that case, the repair would happen on-site and maybe take an hour or two. In my experience, this even worked while traveling to another country. Sometimes manufacturers would also send you a replacement part and you could replace it yourself (happened to me with a failed hard drive).

Grades don't actually matter that much for admissions. The letters of recommendation are much more important, e.g. from the advisor that you did your thesis with.

Voice transcription is not always an option. It works decently for English if you are only using it to transcribe simple, daily texts and you are not in public. For other languages or more complex topics, you quickly hit the limit of what voice transcription can do. In public, you may also not want to say everything out loud that you are about to text to someone.

That actually depends on the logic being used. Some of the logics supported by Z3 are not even decidable. In fact, even solving quantifier-free bit-vector formulas is NEXPTIME-complete [0] when using a binary encoding.

[0] http://smt2012.loria.fr/paper7.pdf