kdavis

6 ms·

1.
by kdavis 5d ago
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
2.
by kdavis 5d ago
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 &q
3.
by kdavis 8d ago
All your datum are belong to us!
4.
by kdavis 9d ago
"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] http
5.
by kdavis 9d ago
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?
6.
by kdavis 10d ago
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 consequen
7.
by kdavis 10d ago
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&#x27
8.
by kdavis 10d ago
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?
9.
by kdavis 12d ago
Impressive! Buzzard's group[1] got scooped. [1] https://github.com/ImperialCollegeLondon/FLT
10.
by kdavis 1mo ago
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 go
11.
by kdavis 1mo ago
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 protecti
12.
by kdavis 1mo ago
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.wikipe
13.
by kdavis 1mo ago
Donald, is that you?
14.
by kdavis 1mo ago
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 simulat
15.
by kdavis 2mo ago
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&#x
16.
by kdavis 2mo ago
https://news.ycombinator.com/item?id=49111599
17.
by kdavis 2mo ago
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
18.
by kdavis 2mo ago
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
19.
by kdavis 2mo ago
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 be
20.
by kdavis 2mo ago
"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/
21.
by kdavis 2mo ago
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.
22.
by kdavis 2mo ago
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.
23.
by kdavis 2mo ago
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
24.
by kdavis 2mo ago
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 includ
25.
by kdavis 2mo ago
Trephination! :-) [1] https://en.wikipedia.org/wiki/Trepanning
26.
by kdavis 2mo ago
Surgery, antimicrobials, farming crops, animal husbandry... humans are late to the game.
27.
by kdavis 3mo ago
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.
28.
by kdavis 3mo ago
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) -
29.
by kdavis 3mo ago
What other verification targets did you consider?
30.
by kdavis 4mo ago
Surprised pikachu face

More ›