Jaxan

I have a surface pro 4 and absolutely like touch. The combination of an actual keyboard and touch is very efficient.

I’ve always used parser combinaties in Haskell and I’ve never seen the things you describe. I guess in Haskell one always directly apply the parts to the function you want (ie an AST node constructor).

> i think for an experienced developer using claude the app itself would be easy to build

Maybe. But if everyone has to vibe code this themselves, it would be a hugely inefficient endeavour. Better to share these projects and help others!

I remember a rock paper scissors AI decades ago that did something similar.

> you can't have upper bound without breaking Turing and solving halting problem

Not in general, no. But for a fixed n, you can. For example, people have settled the exact value of BB(5).

First, an upper bound would be more useful to understand BB. But second, out of all large numbers, does this one give any information? We’ll have to see. The fact in itself is useless.

I don’t think such a bound in itself is interesting, unless the proof reveals some strategy to prove more. There are infinitely potential bounds to BB(n), why is this particular case BB(10) > G useful for understanding fast growing functions?

Oh, as soon as you add tls to your subdomain, the bots come. It’s instant.

It does have S/MIME, I think?

They mean a different statement, a different theorem. You have to understand that translating a theorem written in English text to lean code is also a non trivial step.

But it has. Think of design patterns and other programming paradigms (logic programming, functional programming, etc).

As someone who grew up with Milkdrop, these seem a bit dull/minimalistic.

Not only that, we also have code comments and standalone documentation.

You still need a mathematician to check the statement of the theorem.

Can’t you just open a folder inside your Dropbox folders? Then it should just sync, right?

(That’s how I use zettlr, but with nextcloud instead of Dropbox.)

Indeed, and also:

> and like most I used Apple Notes.

Most people i know that write more then just some notes use obsidian, zettlr, … or one of many other markdown editors.

A comparison with existing apps would be nice.

The caption on the close up says: “Details preserved on both face, face in the back in focus”. But it seems to me that a lot of detail is actually missing! On the later pictures you see a lot of skin “imperfections”, which looks much better. The 18 pro picture is way too smooth!

Wouldn’t it be just as easy to keep Fortran alive with ai?

I agree. But it’s cool to explore these things and if it’s the first time someone sees it, that’s nice!

But if you program a for loop computing the sum from 1 to n, this also gets replaced by a constant (unless you build in debug mode). Why would an empty loop be different?

Yes. A lot is not accessible if not logged in.

Doesn’t help with scrapers though. They use a unique IP for each query.

Sometimes you can use SMT for “theorem proving”. It is a rather broad term. I don’t think they added something much different than what they already had.

With human proofs, I have some trust in process behind it.

The recent proof of Fermats Last Theorem is interesting: it is (iirc) 13 million lines of lean code. And type-checking takes 5 hours or so on a pretty beefy machine. I cannot independently verify the proof, and I have to take Anthropics word for it that it actually type-checks.

I looked in the AppStore for “symmetry draw”, and there are at least 10 such apps.

Wouldn’t a lot already be in leans mathlib?

Most systems i have seen are way beyond a 100 lines. And their GitHub repository contain many issues, often soundness bugs. (Granted, many get fixed very fast.)

This is a crucial point. There have been many bugs in Lean (and in other proof assistants for that matter). Proof assistants work well on human input, because it was created with a certain intent.

We simply don’t know what those 13M contain and whether it “makes sense” and doesn’t trigger Lean bugs. (There are “independent” lean verifiers, but historically they contained the same, or similar, bugs.)

I guess it’s submitted for the method rather than the result.