So, the specification of the theorem we are fairly solid on, formalising what a group is, and a simple group, have been done a long time and we are confident in the correctness of.
Assuming you do trust those, then assuming the formalisation passes lean (and lean has no bugs!), then the whole idea is you've got a proof of the theorem.
Yeah obviously that's the absolving theory - that's how a control works. Basic stuff. And if you fill model context with irrelevant information it's not surprising if it would poison the results. It could certainly be an alignment thing, or something malicious. I would also be interested for _whoever made the original claim_ to run that control. Because that's how science works. Because burden of proof is on who makes the claim. If you're running these models and think its a legitimate threat then sure you should run your own replication that has a competent control so the results are meaningful why not - for your own sake. Otherwise burden of proof is on whoever makes the claim. It that's you and it's trivial to conduct - go for it and let us know what you find!
Not if they get told they are clear. Then their cancer gets worse and before anyone realises it’s untreatable. Downplaying faked test results is disturbing.
1) We have a legal system which (not perfectly) can reverse or fix issues which arise, with crypto money, it's just gone.
2) Someone who can produce fake colourful paper will typically only be able to produce a fairly small amount and not destabilize the whole currency. In the rare occurrences where someone found a significant hack in a crypto-currency, it's just done.
(The bug is they do 'clever matching', so wedding matches weds, and too many emails you weds for wednesday, you can't say 'just show the word I ask you for')
I just checked (the desktop version) and right clicking and using "search messages" also does not use the global index and does not do stemming. It is sieve, which has issues (no way to search based on DMARC authenticated exact email address, which is something basic that email search should really provide) but does cover a lot of search. You can save common searches as folders, though frustratingly "search messages" does not appear on those saved searches; it would be quite convenient if it did and started a search pre-filling the saved settings. I had actually forgotten that the global search exists so I turned it off (at the bottom of general settings).
If you sort by relevance it seems to prioritise the word you asked for? I searched "wedding" and the first few hundred results were all emails about actual weddings. It was only when I sorted by date I saw the "Wed" results.
Many such cases. Duckduckgo is practically unusable because it just decides for itself which of my search terms it actually searches for. I have to explicitly quote every word to get it to function like a search engine.
Meanwhile, Netflix search (on Apple TV at least), is not only practically unusable, but literally so. Doesn't matter what you input, it just returns a random selection of films. I saw Kill Bill the other day, and wondered if there were any other Tarantino films on there. "Tarantino" returned things like Indiana Jones and other completely nonsensical results.
Netflix used to have codes you can search that were by category. I think it might work work on browser. Was a much better way to discover stuff (there's way more categories than you would expect)
Searching the same codes on an Apple TV is a very weird experience. It seems to sort of start to recognise what you're doing and then also give you a random assortment of the same crap it thinks your account wants to see.
I agree that word is bad, but I don't think we have a great replacement yet.
Markdown -- standard markdown isn't expressive enough (no tables for example), there are lots of extensions but none which are "standard".
LaTeX -- doesn't produce accessible documents, so is a non-starter in lots of areas (seriously, the PDFs it generates are some of the worst around when it comes to accessibility. Word's are amazing).
If we put aside the Word file format, and maybe the ribbon, is Word bad though?
I've been using it for decades, and have tried OpenOffice and LibreOffice too over the years - nothing comes close to Word.
Markdown is not suitable for "normal" users, but as a developer, I've come to prefer markdown for technical documentation and such (especially where I want a history, diffs etc), but I still use Word for a lot of other things.
Word is incredibly fully-featured - I use a lot of functionality, but am likely still only using a fraction of what it has. It really does have all your document editing needs covered.
Aside from the file format, I think Word is a fantastic piece of software. I have a few annoyances with it now and then, but it's been very dependable and kept me in good stead over the years.
> If we put aside the Word file format, and maybe the ribbon, is Word bad though?
Is the ribbon bad, though, or are we just living through 2003 era UI shock for 13 years now?
I lambasted the ribbon as was fashionable back then, but actually using it in 2020?
It's good. Like, legit amazing UI design. Makes it easy to peck through menus and find what you want. Structures chords for power users, and importantly makes those chords visually discoverable. I've found a pile of good keyboard shortcuts just by starting to slowly press a chord on the ribbon.
It's great for mouse users.
It's great for noobs just learning the ropes.
It's great for keyboard users who already know their stuff.
It's amazing at facilitating the learning process into knowing your stuff
It's been great for 17 years. Do we still have to pretend it sucks because we were used to a different way of doing things?
I said that because I know the ribbon is still contraversial, and some people still don't like - personally, I've come to like it, if not love it as you have.
Irritatingly, even if you upgrade to the very latest Mac OS X and Xcode, you still get Python 3.9.6.
While you can give people guidance to install a more up-to-date python, everything is much, much harder than the default experience that gives them 3.9.6 (and also once you have them running a custom version with uv or something, may as well just get them to install 3.15!)
This is very deliberate: included scripting runtimes for Python, Ruby are only for compatibility with legacy software, not for any new development. This goes back as far as macOS 10.15 from 2019 [1].
They still haven't gotten around to actually removing them (probably don't want to deal with support/complains), but keeping versions pinned to ancient versions will naturally nudge developers to take care of their own runtime requirements. (They do the same with bash, perl, ruby.)
No, this is not true. macOS 10.15 included Python 2.7 as part of the OS, and it was removed in macOS 12.2 IIRC.
Python 3.9 is still included in Xcode and the Command Line Tools, but not the OS itself. It’s only for running scripts (and for supporting LLDB I think), applications cannot link against it like they could with the old OS-bundled 2.7.
Python 3.9 is getting conspicuously old though, I was a bit surprised Apple didn’t update it in Xcode 27.
> on Solaris, unlike elsewhere, the packaging system is intended only for system components (and Solaris defines this narrowly), not additional software.
I know Python versions and dependency management is always awkward for people who don't use it every day, but you should almost never use the bundled version of Python on the system, and instead pin a dedicated version for whatever you're developing. And use a virtual environment. uv solves all of this.
> may as well just get them to install 3.15
Exactly. If the project you're trying to run needs a certain version of Python, it's no concern of the system that you're running on, it's a concern of the environment you're running in.
C build environments and linked libraries don't do this, and it's one of the reasons why I am a fan of isolated Python environments. You can't get into dependency conflict resolution hell if the dependencies are defined by a single system.
Why would the Europeans want a high-quality open source model that isn't either owned by American Trillion-dollar companies or created by the Chinese? You really can't think of any reasons?
I don't know what definition of open weights you are using, but the "open" part is what allows you to use it without being beholden to American Trillion-dollar companies or the Chinese.
Mistral could do exactly what Cursor does, and post-train the model to meet the needs of Europeans.
That's a far more efficient (and useful!) use of GPUs than yet another pretrain on an outdated model backbone.
What happens if Mistral stopped trying to make foundation models, and then China stopped releasing their open weight models?
It's core to their whole value proposition that they are providing sovereign AI capabilities in Europe. If they're just repackaging Chinese models they don't really provide that sovereignty, and they'd be unable to justify their valuation or investments.
I'd prefer a mid open model as an option, Anthropic + OpenAI are already hiking prices, what when they decide to collude and hike them 100x at some point in the future? I'll be happy with a mid open alternative then.
> You do realize that China is not the only place making open weights models, right?
It's the only place making open weight models close to competitive with American closed-weight models, and the only open-weight models that beat Mistral's models.
> I don't think they're justified now, certainly their results don't justify it. Mistral is mid at best.
Their investors and customers disagree.
> Except they don't, they are dependent on GPUs from nVidia and AMD—both American companies.
That's a pre-existing dependency that nobody in Europe is happy about. The goal with Mistral is to avoid there being yet another new layer of outside dependency. Mistral isn't a GPU company and isn't trying to be.
However, if someone in Europe was able to build a GPU that's as close to Nvidia or AMD as Mistral is to Anthropic or OpenAI, that company would also be seeing a lot of keen interest and likely piles of money.
Assuming you do trust those, then assuming the formalisation passes lean (and lean has no bugs!), then the whole idea is you've got a proof of the theorem.
reply