seeknotfind

I would worry more about 5D chess or 6D and even 7D chess. This article talks about teaching models to be good and methods that could train goodness, but it sounds like there are some unsolved problems to graduate to 8D+ chess.

Is this supposed to be scary or amazing?

Wow. This is incredible. Turning the entire field of mathematics into a formalized and connected system. An index of mathematical understanding. All fields will undergo this change!!!

My man Terrance Tao, I hope to contribute to your symphony of progress.

If the interrelationships of this are also exposed and searchable, if it can build many bridges inside itself, then this is truly the cipher key to all that can be known.

100%. Context is big for AI, but it's nothing compared to everything a human can learn. If you efficiently represent everything in context, it may be many papers, but if AI is actively working through proofs, it will quickly fill up. They're no denying AI is making strides, but pinning it to memory is an oversimplification.

We are?

If you're calling this across translation units, the calling convention will come with a performance penalty, but boy have we come full circle since pre-ANSI C required you to pass args as a struct. Much love - wish the language required struct and arg list to be the same thing. You can send a list of em and it'll work with algebraic data types for batching calls. The dream. CPU doesn't play nice though since structs aren't register shaped, but maybe they could be in a future calling convention.

You can click on that to see more detail :)

"I'm sorry". What do HN readers think about how this inclusion changes the meaning of the rest of the email?

Did you ever try multiple copies?

They're are plenty of mods that inject AI into games, like Skyrim. Though in order for a game to have LLMs and scale to a shipping audience without a subscription, you would want to run them locally.

The real technical blocker is performance and voice synthesis. If voice synthesis was at parity with human actors, it would be worth it to battle the performance aspect for major studios. In text based games especially, taking time to generate enough text is just too slow to be convenient

Very cool. Can't wait to see what's next with this project! Congrats on the huge scale of tests/examples as well.

Thanks, yeah, I did see some of the pure C++ types getting converted. Though it makes a lot of sense why you had to go with shared_ptr for generic inductive types.

Have you considered combinatorial testing? Test code generation for each sample program, for each set of mappings, and ensure they all have the same behavior. If you look at the relative size or performance, it could allow you to automatically discover this issue. Also, allocation counting.

Hey also sucks you are not in SF. I'm looking for people into formalization in the area, but I haven't found any yet

From tests/basics/levenshtein/levenshtein.cpp:

    struct Ascii {
      std::shared_ptr<Bool0::bool0> _a0;
      std::shared_ptr<Bool0::bool0> _a1;
      std::shared_ptr<Bool0::bool0> _a2;
      std::shared_ptr<Bool0::bool0> _a3;
      std::shared_ptr<Bool0::bool0> _a4;
      std::shared_ptr<Bool0::bool0> _a5;
      std::shared_ptr<Bool0::bool0> _a6;
      std::shared_ptr<Bool0::bool0> _a7;
    };

This is ... okay, if you like formal systems, but I wouldn't call it performant. Depending on what you are doing, this might be performant. It might be performant compared to other formally verified alternatives. It's certainly a lot nicer than trying to verify something already written in C++, which is just messy.

From theories/Mapping/NatIntStd.v:

    - Since [int] is bounded while [nat] is (theoretically) infinite,
    you have to make sure by yourself that your program will not
    manipulate numbers greater than [max_int]. Otherwise you should
    consider the translation of [nat] into [big_int].

One of the things formal verification people complain about is that ARM doesn't have a standard memory model, or CPU cache coherence is hard to model. I don't think that's what this project is about. This project is having basically provable code. They also say this in their wiki:

https://github.com/bloomberg/crane/wiki/Design-Principles#4-...

> Crane deliberately does not start from a fully verified compiler pipeline in the style of CompCert.

What this means is that you can formalize things, and you can have assurances, but then sometimes things may still break in weird ways if you do weird things? Well, that happens no matter what you do. This is a noble effort bridging two worlds. It's cool. It's refreshing to see a "simpler" approach. Get some of the benefits of formal verification without all the hassle.

> Composition is like applying a permutation array to another

Composing injective functions is like applying a permutation array to another.

I bought several of these and give them as gifts. Unix Pipe, Expansion Pack, and PUNK0 are my favorites.

Yeah, from the title, it sounds like perhaps the entire operation is differentiable and therefore trainable as a whole model and that such training is done. However, upon close inspection, I can't find any evidence that more is done than calling the model repeatedly.

Yeah, it sounds platonic the way it's written, but it seems more like a hyped model compression technique.

I suspect that once quantum computers actually scale up so that you can play with them, we'll find all sorts of interesting things to do with them.

However, even now, you can imagine that if quantum computers were small enough, it would be worth it to have it just for the asymptotically fast prime generation with Shor's algorithm. I don't think that's that far fetched. Of course, people wouldn't necessarily need to know they have a quantum computer, but they don't necessarily know the workings of their computers today anyway.

The last digit of pi doesn't exist since it's irrational. Chaitan's constant, later busy beaver numbers, or any number of functions may be uncomputable, but since they are uncomputable, I'd be assuming that their realizations don't exist. Sure, we can talk about the concept, and they have a meaning in the formal system, but that's precisely what I'm saying: they don't exist in this world. They only exist as an idea.

Say for instance that you could arrange quarks in some way, and out pops, from the fabric of the universe, a way to find the next busy beaver numbers. Well, we'd be really feeling sorry then, not least because "computable" would turn out to be a misnomer in the formalism, and we'd have to call this clever party trick "mega"-computable. We'd have discovered something that exists beyond turing machines, we'd have discovered, say, a "Turing Oracle". Then, we'd be able to "mega"-compute these constants. Another reason we'd really feel sorry is because it would break all our crypto.

However, that's different than the "idea of Chaitan's constant" existing. That is, the idea exists, but we can't compute the actual constant itself, we only have a metaphor for it.

Do you mean like ghosts or like quantum randomness and Heisenberg's uncertainty principle?

We cannot compute exactly what happens because we don't know what it is, and there's randomness. Superdeterminism is a common cop out to this. However, when I am talking about whether something is computable, I mean whether that interaction produces a result that is more complicated than a turing complete computer can produce. If it's random, it can't be predicted. So perhaps a more precise statement would be, my default assumption is that "similar" enough realities or sequences of events can be computed, given access to randomness, where "similar" is defined by an ability to distinguish this similulation from reality by any means.

As the simplest theory, my default position is the universe is computable and that everything in the universe is computable. Note that they are not the same thing.

Some intuition:

1. If the universe contains an uncomputable thing, then you could utilize this to build a super turing complete computer. This would only make CS more interesting.

2. If the universe extends beyond the observable universe, and it's infinite, and on some level it exists, and there is some way that we know it all moves forward (not necessarily time, as it's uneven), but that's an infinite amount of information, which can never be stepped forward at once (so it's not computable). The paper itself touches on this, requiring time not to break down. Though it may be the case, the universe does not "step" infinitely much information.

One quick side, this paper uses a proof with model theory. I stumbled upon this subfield of mathematics a few weeks ago, and I deeply regret not learning about it during my time studying formal systems/type theory. If you're interested in CS or math, make sure you know the compactness theorem.

Paper direct:

https://jhap.du.ac.ir/article_488.html

I enjoyed some commentary here:

https://www.reddit.com/r/badmathematics/comments/1om3u47/pub...

See also:

https://en.wikipedia.org/wiki/Mathematical_universe_hypothes...

I'm looking forward to seeing everyone coming up together, creating better fonts for free, and wiping out any of those profits. Is Monotype trying to destroy their own industry, or do they really think this will work?

How many times does the rate need to be increased 10x before it's a problem?

Yeah, people tend to add rather than improve. It's possible to add into lower levels without breaking things, but it's hard. Growing up as a programmer, I was taught UNUX philosophy as a golden rule, but there are sharp corners on this one:

To do a new job, build afresh rather than complicate old programs by adding new "features".

"It’s not likely to be something you’ll ever have at home" Pessimistic much?

Thousand of hours on this. Love it.

It's nice that there is only a few weird behaviors produced. Often use-after-free leads to so many different random bugs, you might gorble a hubalu.

"Xia" would map to a single character (code point) in Chinese. For instance, in simplified Chinese, it could be 下 (xia, meaning down), 侠 (martial arts - like the xia in wuxia), or any number of other homophones. Since the characters are already combinatorial, I'm not sure a Chinese speaker would think of this as a portmanteau.

If you've seen Steve Martin's The Jerk, you'd know he becomes a real jerk in the modern sense during the movie.

I didn't see the con explicitly in the comments. When someone adds a file, they'll have trouble figuring it out why it's not visible in git, or they may not realize an important file is missing if they are adding multiple.