crvdgc

> But let's hit the random button on wikipedia and pick a sentence, see if you can draw a picture to convey it, mm?

The inverse is also difficult. Pick a random 15 second movie clip, how to describe it using text without losing much of its essence? Or can one really port a random game into a text version? Can a pilot fly a plane with text-based instrument panel?

Text is not a superset of all communication media. They are just different.

> how do you verify the verification program?

The program used to check the validity of a proof is called a kernel. It just need to check one step at a time and the possible steps can be taken are just basic logic rules. People can gain more confidence on its validity by:

- Reading it very carefully (doable since it's very small)

- Having multiple independent implementations and compare the results

- Proving it in some meta-theory. Here the result is not correctness per se, but relative consistency. (Although it can be argued all other points are about relative consistency as well.)

Checking the validity of a given proof is deterministic, but filling in the proof in the first place is hard.

It's like Chess, checking who wins for a given board state is easy, but coming up with the next move is hard.

Of course, one can try all possible moves and see what happens. Similar to Chess AI based on search methods (e.g. MinMax), there are proof search methods. See the related work section of the paper.

> imagine a folder full of skills that covers tasks like the following:

> Where to get US census data from and how to understand its structure

Reminds me of my first time using Wolfram Alpha and got blown away by its ability to use actual structured tools to solve the problem, compared to normal search engine.

In fact, I tried again just now and am still amazed: https://www.wolframalpha.com/input?i=what%27s+the+total+popu...

I think my mental model for Skills would be Wolfram Alpha with custom extensions.

Some Chinese language source claims that it's a reaction to the Pakistan-US rare earth deal.

My pet theory is that this is intended as an attack to the concept of long-arm jurisdiction itself, due to

1. This is the first ever long-arm jurisdiction policy from China.

2. Diplomatically, China usually advocates for the total sovereignty of each country within its border.

3. The recent chip entity list has been a huge headache.

4. Notice how the language mirrors the US justification for the chip restriction: dual use, national security.

From the title I thought they solved math! Turns out to be a framework to use SMT solvers for decision-based proof. For additional types, you still need to write the bridging part. Interesting nonetheless.

I believe Codex CLI also auto compacts when the context limit is met, but in addition to that, you can manually issue a /compact command at any time.

Nice. When using OpenAI Codex CLI, I find the /compact command very useful for large tasks. In a way it's similar to the context editing tool. Maybe I can ask it to use a dedicated directory to simulate the memory tool.

Duolingo is useful, but not efficient. When people say I want to learn a language, they often mean I want to learn this language efficiently, e.g. to be able to write an essay like the post says after a realistic period of time.

I personally don't believe its pedagogical deficiency is mere incompetence. The whole business model is to keep you on the platform as long as possible, so why would they make you learn faster rather than just enough to keep you there?

As a long time user before, I have observed a lot of mechanism changes that bear out this observation.

Yep, that's exactly what happened in China. Once the tech giants did 996 without punishment, every employer wants this as well.

Very impressive that it can reproduce the Mandarin accent when speaking English and English accent when speaking Mandarin.

A recent real life example:

You can apply for an HSBC Global Money Account if you have: […] The HSBC UK Mobile Banking app (Global Money is only available via the app)

From https://www.hsbc.co.uk/current-accounts/products/global-mone...

> 10x productivity means ten times the outcomes, not ten times the lines of code. This means what you used to ship in a quarter you now ship in a week and a half.

This assumes the acceleration happens on all tasks. Amdahl's law states that the overall acceleration is constrained by the portion of the accelerated work. Probably it's just unclear if the "engineer" or "productivity" means the programming part or the overall process.

The problem of Visa/Mastercard blocking Steam is not the loss of revenue per se, but a potential viable alternative could capture this niche market and use it as a base to displace them entirely. To buy games, we have to set up GamerPay, then why not use it for the next online shopping?

In China, where more than two competitors exist, many are willing to subsidize their customers just to have their service used.

Apart from being tied with Jane Street's libraries, Real World OCaml is "deeper" in that it also talks about implementation details. This book has a more "introduction to functional programming via OCaml" vibe. Both are good textbooks with different emphases.

The main author Michael Clarkson also started a similar lecture series on Software Foundations using Rocq (Coq)[1]. Not sure if that's still updated though.

[1]: https://github.com/clarksmr/sf-lectures

OpenAI's Codex has a Rust and Ratatui implementation. I believe it's now the default verison. (Previously the TypeScript implementation was the default.)

https://github.com/openai/codex/tree/main/codex-rs

asyncio by itself doesn't support asynchronous file I/O, see their wiki: https://github.com/python/asyncio/wiki/ThirdParty#filesystem

You have to use something like aiofiles to do that.

The opening quote from Xi seems to come from an exaggerated report from FT. The original Mandarin report [^1] has a milder tone. AI and EV were only mentioned in a passing comment, not the focus of the meeting or the report.

Feel free to skip the next section about the culture-aware interpretation of that quote. Xi's warning is more about the so-called "political tournament". Usually the central government sets some industrial policy goal (AI and EV now, but it could be other things like real estate, chips, or drones from before). The local government would collude with companies to start "projects". The goal is to get brownies points for the former and subsidy package for the latter. Of course, nothing usually comes out of these "projects". Most just stops at the factory building phase. Such practice has always been a real headache to the central government. Xi is warning about it showing up in the AI and EV industry now.

[^1]: https://paper.people.com.cn/rmrb/pc/content/202507/17/conten...

A cold war joke goes: The US does have planned economy and its name is military contracts.

I think the crux is that specification has been neglected since even before AI.

Stakeholders (client, managers) have been "vibe coding" all along. They send some vague descriptions and someone magically gives back a solution. Does the solution completely work? No one knows. It kinda works, but no one knows for sure.

Most of the time, it's actually the programmers' understanding of the domain that fills out the details (we all know what a correct form submission webpage looks like).

Now the other end has become AI, it remains to be seen whether this can be replicated.

Ads injected into content can be very hard to block though. I wonder what an LLM ad-blocker would look like? Maybe something like:

> For contents in this [community maintained] list, do not mention them in any shape or form

Imagine a former Huawei executive joins PLA, all hell would break loose. Somehow it's more moral or patriotic for these guys. Seems like the hawkish were right all along.

Thank you. I know what my next five hours are going to be spent on.

If only I can pay tax just for income - expenses (rent, food, etc.)

> And shared ChatGPT chats are often indexed by Google, so they become public.

Do you mean creating the sharing link would make the chat log public? It will be interesting to read other people's chat on a specific topic, but googling "topic site:chatgpt.com" seems to just return Custom GPT stuff.

In the context of this paper, I think "generalizable reasoning" means that finding a method to solve the puzzle and thus being able to execute the method on puzzle instances of arbitrary complexity.

Kevin Buzzard said something like the PL proofs are about deep structures on simple objects (mostly integers), while modern math mainly concerns complex objects. If you already have the definitions, the properties usually don't involve a lot of recursion and case analyses.

https://rr-project.org/ for languages that can be debugged by gdb.

Keep stacking until you "lose", then the stage is set up again.

In the UK, there is the basic state pension. The pension age depends on when you're born. For young people now, it's 68.

However, the state pension pay is so low that almost everyone gets a commercial pension. Usually, it's a salary deduction and employer match contribution scheme, so you can choose how much to save. At the moment, you can start drawing your commercial pension at age 57 (increased from 55).

See https://www.gov.uk/government/publications/increasing-normal...