mdnahas

I worked on formal proof in 2014, but abandoned it when I realized academic mathematicians would never use it. Formal proof would have helped math’s consumers: better search, fewer mistakes, easier translation (to other human languages), etc.. But academic mathematicians didn’t care about math’s users very much.

Now that there are tools that help math’s consumers and because the economy of proof production wasn’t oriented towards consumers, there is a real chance that academic mathematicians get sidelined.

A sweet video showing an inventor did love his wife.

From the Halloween episode of comedy show Saturday Night Live.

Beautiful tribute montage.

As I heard it, Germany refused to carry the Usenet channel alt.sexy.bald.captain because the thought it was porn. It was a Picard fan club.

The market way to deal with outliers is to have an options market. Basically, it is an insurance market for providing electricity on a tight day. Texas has a different way of handling it that I don’t like.

A big problem in the electricity market is that most customers don’t respond to supply shocks. They pay the same price in an emergency as in normal times. So, when it got very cold and power plants started shutting down, they used more electricity because they needed more heat! The one electricity provider who did pass on higher prices to customers and reduced consumption, Griddy Energy, was roasted in the media. Because customers didn’t respond to the shortage, utilities had to. They instituted “rolling blackouts”, which we really just blackouts for any grid that didn’t have a hospital on it.

As an economist, I wondered what the capitalist equivalent of communist central planners would be. Sometimes it is futures markets and sometimes it’s consultants like McKinsey. They are a way of passing information between competitors in a market, to achieve controlled growth, market segmentation, etc.

They also serve as a part-time strategy group for the company. The company couldn’t afford that quality of people full time and they wouldn’t have as much experience as at a consultancy. And having temporary people not beholden to a superior might result in more honest reports.

So, it’s not necessarily flimflam. But I do worry a group of people who determine a company’s strategy and rarely stick around to implement it and measure it’s end result.

My thought: Claude may not have fixed the bugs, but avoided the problem for the poster’s use cases. “Fixing a bug”, in my mind, means solving all problems for all use cases. And Claude didn’t have to do that.

The insertion of NOPs is a great way to remove a function call that might have crashed the program. If you didn’t need anything that function did, you’ve solved your problem but not fixed the bug.

It varies by car. For my Honda, I believe disconnecting the antenna is enough. I looked at a Toyota and the antenna is shared. To disable the phone-home you had to disconnect a box … but that’s difficult. The box is also designed to call 911 or 999 emergency services and is connected to the microphone and one of the speakers. You have to rewire those if you want to use the microphone with your cellphone or play any stereo sound. Do your research before buying or disconnecting things.

Yes, that’s very true. I recognized that in 2014. It was hard, but I stopped doing research on formal proof.

I got an economics degree and found that the City of Austin to pay off its $3 billion dollar pension debt … and encountered the same problem you mentioned, again. Except this time my plan is to run for City Council and be their next-level superior.

As a consumer of mathematics, I want to attack the author’s idea of “what that work was meant to achieve in the first place”.

I do a lot of programming that uses mathematics. I designed the error recovery file format “par2”. I worked as a quantitative trader.

What do I want from math? To be able to search math results, understand them, and apply them. But academic mathematicians are so inwardly focused - as these authors so obviously are - that it does all of these badly! Search is still with words, not symbols and formulae. As for comprehension, many math papers are unreadable to those not in the cliche of mathematicians in that specialty. And even applied math papers don’t ship code or specify the operations explicitly.

I wanted to fix this and in 2013 I worked on formal proof. It makes symbol search and application easy. I found out that the tools had been usable for decades at that point. But mathematicians didn’t use them because they had that inward focus and didn’t give a damn about math consumers.

AI is enabling formal proof. It will carry mathematics into the computer age, which the field should have joined with every other industry in the 1970’s! I welcome it. Math will get used more and that is what the work was meant to achieve in the first place.

A businessman I talked to said that United is investing in smaller airplane manufacturers in hopes of breaking the Boeing-AirBus duopoly. Thus, giving commitments here and to Boom Supersonic.

I just looked at Strawberry. Spotify is done via a GStreamer plug-in. It looks like you have to compile it yourself.

I know someone who calls it “Scamerica”.

One cause is Congress not doing its job for 30 years. The other is the advertising funding model - website users are not the customers. Therefore, websites - especially news sites - aren’t delivering useful information to their users because that doesn’t make more money.

Therefore author is right. Reinforcement learning with this ecosystem is dangerous.