They came to do a "deep dive" developers' workshop with us and all the materials were things that are literally on their public website. Let that sink in: Their idea of a deep dive for developers was to have some sales guy read us parts of their website.

You know the linux kernel is a free software project right? If you think “somebody should” do a thing but you aren’t prepared to do it yourself then you should maybe ask for a full refund.

Thank you very much, seanhunter. You hit the nail on the head there.

Not really, because they made Linux a CNA specifically to own the process and distort it the way they want it to be.

That is not at all how it was and this is strangely similar to the (also untrue) astroturf narrative that got repeated about Martin Shkreli after he got imprisoned for fraud.

FTX users lost money to Alameda by Alameda being able to trade without collateral. He literally stole money from users of his exchange by allowing this.

It absolutely is not lack of rigor and discipline - He was dishonest about it.

Having met Boris Johnson, spoken with people who were at school and at university with him I can say with complete conviction that he is nowhere near smart enough for that. There never was any kind of strategy, he just bounced along from one thing to the next saying the first thing that popped into his head with the carefree conviction of a bear ransacking a picnic hamper and leaving a trail of destruction in its wake.

I met him because I had to give him a software demo at number 10 as part of London Tech week. One of the other teams there had some sort of childrens’ app and got him enthusiastically doing star jumps. Just a complete clown through and through.

or just type "fc" to edit the previous command.

It's not. He vandalised wikipedia and then talked about LLMs in his writeup to gain attention.

…And at this point probably not one but two 9s (or possibly more) of security vulnerabilities [1]

[1] https://securitylab.github.com/resources/github-actions-prev...

In contrast, I asked it about the lumeniferous aether and the Michelson-Morley experiment (which was late 19th C) and it said the aether was not disproved by the experiment (even though special relativity was like 1905 or something).

So definitely the event horizon of the model’s knowledge is a bit porous/nonspecific in either direction.

Intuitionism is just disallowing the law of the excluded middle (that propositions are either true or they are not true). Disallowing non-constructive proofs is a related system to intuitionism called “constructivism”. There are rigorous formulations of mathematics that are constructive, intuitionist or even strict finitist.

What point are you responding to?

THe parent of my post referred to disallowing non-constructive proofs, which is not a feature of intuitionist logic but of constructivism.

It’s not intuitive, it’s intuitionist. I’m not saying that to nitpick it’s just important to make the distinction in this case because it really isn’t intuitive at all in the usual sense.

Why you would use it is it’s an alternative axiomatic framework so you get different results. The analogy is in geometry if you exclude the parallel postulate but use all of the other axioms from Euclid you get hyperbolic geometry. It’s a different geometry and is a worthy subject of study. One isn’t right and the other wrong, although people get very het up about intuitionism and other alternative axiomatic frameworks in mathematics like constructivism and finitism.

> if you exclude the parallel postulate but use all of the other axioms from Euclid you get hyperbolic geometry

No, you don't.

(You need to replace the parallel postulate with a different one)

Thank you for the correction I actually didn't realise that so have learned something.

Specifically for people who are interested it seems you have to replace the parallel postulate with a postulate that says every point is a saddle point (which is like the centre point of a pringle if you know what that looks like).

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

You can also replace it with a different postulate and get projective geometry, IIRC.

I think they called it intuitive, because I called it intuitive in my original post, so that's on me :)

I thought of a concrete example of why you might use intuitionist logic. Take for example the “Liar’s paradox”, which centres around a proposition such as

A: this statement (A) is false

In classical logic, statements are either true or false. So suppose A is true. If A is true, then it therefore must be false. But suppose A is false. Well if it is false then when it says it is false it is correct and therefore must be true.

Now there are various ways in classical logic [1] to resolve this paradox but in general there is a category of things for which the law of the excluded middle seems unsatisfactory. So intuitionist logic would allow you to say that A is neither true nor false, and working in that framework would allow you to derive different results from what you would get in classical logic.

It’s important to realise that when you use a different axiomatic framework the results you derive may only be valid in the alternative axiomatic system though, and not in general. Lean (to bring this back to the topic of TFA) allows you to check what axioms you are using for a given proof by doing `#print axioms`. https://lean-lang.org/doc/reference/latest/ValidatingProofs/...

[1] eg you can say that all statements include an implicit assertion of their own truth. So if I say “2 + 2 = 4” I am really saying “it is true that 2+2=4”. So the statement A resolves to “This statement is true and this statement is false”, which is therefore just false in classical logic and not any kind of paradox.