kdavis

Unfortunately moderated out of existence in 10, 9, 8, 7....

I don't have access to the entire article, but it doesn't mean much to physics.

Physicists knew Navier-Stokes was an approximation that breaks down at some scale, e.g. the molecular scale. This AI solution just exhibits such a breakdown.

Unfortunately attaching a corporation name to a statement is a large part of the motivation for a company to spend millions on tokens for Lean proofs. It's a marketing/PR spend for them. Without their name attached, the return on investment is far less.

That said there are some efforts in the direction you're suggesting. For example

- [Prove2Me](https://beta.prove2.me) - Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. One creates open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions.

- [Tau Ceti](https://github.com/TauCetiProject/TauCeti) - An AIs-welcome Lean library downstream of Mathlib: AI handle the implementation and review, humans write the roadmaps and review rubrics

Kicked off so many memories...

Early 80's I learned Logo and Basic at a local store that sold Apple computers. It was called "The Logical Choice" and had a classroom tucked away behind a false wall and an English Sheep dog "Sir Isaac Newton" that would hang around the store!

Nice, I just found a story on the store, page 5 of [1].

[1] https://mirrors.apple2.org.za/ftp.apple.asimov.net/documenta...

All your datum are belong to us!

"If you have to ask, you can't afford it." -J.P. Morgan

More seriously, I couldn't find a pricing pager either. However, the "Book a Demo" page[1] is usually a sign that the J.P. Morgan quote applies.

[1] https://www.appliedcompute.com/book-a-demo

While the existing body of work on alternate axioms is tremendous, it's finite. The set of possible axiom systems is infinite. Does current the current body of work cover all consequences of all possible axiom systems?

Looking a bit more into this, it doesn't seem your claim "most of the consequences of additional axioms have been worked out" holds up.

Yes, metamathematics is well-developed, but I don't think that most of the consequences of any particular additional set of axioms have been worked out. Each such new set requires re-deriving all of this alternate mathematics from scratch. This is a lot of work!

So I think my original claim---mathematicians select interesting axioms and AI figures out their implications---still seems a possible way forward.

PS: I'd guess descriptive set theory under determinacy is the one place where projective determinacy, as you stated, pays off.

What name does this "well-developed field of mathematics" go by? (I just want to get a taste of what the field is like.)

I also thought that there are an infinite set of possible extra axioms, e.g. axiomize any statement that's true but not provably so via Gödel's First Incompleteness Theorem, though maybe the vast majority of such axioms are "uninteresting".

Maybe in the future mathematicians could be the ones proposing different axiomatic foundations (e.g. ZF vs ZF + C vs ZF + C + CH vs ...) and then using computers to examine the consequences of these differing foundations?

Impressive! Buzzard's group[1] got scooped.

[1] https://github.com/ImperialCollegeLondon/FLT

It has reached beyond government institutions. From the linked article:

"These policies’ tentacles already extend beyond government websites... Reports say scientists are self-censoring in hopes of improving their chances of getting government grants."

In regards to government institutions, limiting speech in this way will cause people to die.

For example, banning the phrase "air pollution" will curtail efforts to address air pollution, e.g. scientists not submitting research proposals addressing air pollution, causing people to die as a result[1].

[1] https://www.cdc.gov/climate-health/php/effects/air-pollution...

For context on PEN America, from Wikipedia[1]

> PEN America (formerly PEN American Center), founded in 1922, and headquartered in New York City, is a 501(c)(3) nonprofit organization

> whose goal is to raise awareness for the protection of free expression in the United States and worldwide through the advancement of

> literature and human rights.

[1] https://en.wikipedia.org/wiki/PEN_America

I know I'm just an old man yelling at clouds, but the sentence...

"Meta did...kick off the origin of the open source race back in 2023"

ignores the majority of open source software history[1].

[1] https://en.wikipedia.org/wiki/History_of_free_and_open-sourc...

Donald, is that you?

The article seems like an interesting Gedankenexperiment. However, I think it overrotates on the GR analogy.

For example "..ARC captures the logical leap, it misses the manipulative component—the physical sensation and embodied simulation..." makes lots of assumptions on how such a discovery must occur, e.g. through "physical sensation and embodied simulation". Results matter, not the path there.

For example, quantization of energy, at the core of QM, wasn't discovered through "physical sensation and embodied simulation" at all. Planck simply found that if energy is quantized, then one obtained the observed black-body radiation spectrum. There was no "physical sensation and embodied simulation".

Mac User Guide documentation states "When autocorrection is on, misspelled words are detected and automatically corrected as you type."

[1] https://support.apple.com/en-az/guide/mac-help/mchlp2299/mac

Craig Federighi SVP of Software at Apple “The keyboard now leverages a transformer language model, which is state of the art for word prediction, making autocorrect more accurate than ever.”[1]

"New features available with macOS Sonoma" doc states "Autocorrect fixes mistakes for you more accurately than ever before by leveraging a new transformer language model in English, French, and Spanish keyboards." [2]

"Introducing Apple’s On-Device and Server Foundation Models" blog post states "Apple Intelligence is comprised of multiple highly-capable generative models that...have been fine-tuned for user experiences such as writing and refining text.. In the following overview, we will detail how two of these models — a ~3 billion parameter on-device language model, and a larger server-based language model."[3]

"A look at Apple’s new Transformer-powered predictive text model" blog post[4] is the kind of deep dive you'd have to do to find out what's going on under the hood in your spelling/grammar checker. TL;DR AppleSpell uses GPT-2 which proves my point.

[1] https://eu.usatoday.com/story/tech/2023/06/06/wwdc-2023-appl...

[2] https://www.apple.com/mideast/macos/sonoma/pdf/en/macOS_All_...

[3] https://machinelearning.apple.com/research/introducing-apple...

[4] https://jackcook.com/2023/09/08/predictive-text.html

If the company making this claim were not famously litigious, I would agree with your "good faith" interpretation. They are, unfortunately, famously litigious[1].

[1] https://en.wikipedia.org/wiki/Google_LLC_v._Oracle_America,_...

This wasn't your original question, which I answered.

This "moving the goalposts", requiring me to know the internals of say a closed source product, just proves my original point. I can't know if an LLM is being used because I don't have the source code.

"A Simple yet Effective Training-free Prompt-free Approach to Chinese Spelling Correction Based on Large Language Models"[1]

[1] https://aclanthology.org/2024.emnlp-main.966/

I don't know the timeline, but I generally agree.

I think history agrees too, i.e. machine code > assembly language > high-level programming language > prompts.

The is not exactly my point.

I am speaking of spelling/grammar checkers are part of the IDE and/or OS.

You'd have to know your IDE and/or OS's implementation details to know you are not using an LLM based one.

My point is you might be when you wrote your comment or I might be in writing this comment.

However, I don't know if I am as I haven't seen, and will likely never see, the implementation behind the text box that is suggesting the next letter, word, or spelling correction as I type.

While I understand the caution, the current policy seems too draconian.

It states in part:

> Until that policy is in place, the Governing Board has approved this interim policy:

> Contributions in the OpenJDK Community must not include content generated, in part or in full, by large language models...

Note, this would exclude most spell checkers, as they often are LLM based. That said, they do soften this with the addition:

> Q: Is it okay to continue using the spell-checking, grammar-checking, auto-completion, and refactoring features in my editor or IDE?

> A: Yes, so long as they are not based on large language models or similar deep-learning systems.

This addition will likely not help as most spell checkers are OS/IDE services and their implementation details are opaque to users.

Trephination! :-)

[1] https://en.wikipedia.org/wiki/Trepanning

Surgery, antimicrobials, farming crops, animal husbandry... humans are late to the game.

Using gemma3:12b I ran it once over Andrew Ng's CV https://ai.stanford.edu/~ang/curriculum-vitae.pdf because why not.

He's a 48.0/100, things that make you go Hmmm.

Hmm...six runs with gemma3:12b on my CV

- Varies from 102.0/100 to 100.0/100

- Missed lots of OSS work

- Misinterprets GSoC work (Thinks projects I started that were contributed to in GSoC implies that I received a GSoC stipend)

- Areas for improvement seem to vary inconsistently (There's not enough project detail to there's too much project detail)

I still don't make company cut offs ¯\_(ツ)_/¯