The idea of the reverse rug-pull is fantastic, I hope it will work out! The ways people abuse open-source is appalling, yet the risible funding that goes to open-source makes thing really difficult for everyone.
The whole write-up is quite interesting so I'll definitely try it out.
Pangram says 50% human. That seems to check out, heavily edited yet the LLM aha sentences and cadence are still definitely there, but not overbearing.
I read some Dostoevsky recently and I found my speech to be substantially altered for a while, so it makes sense that LLM writing would have an influence.
I wholly empathize with the posts.
Recently my writing process has become much longer as asking for LLM polish leads to spending more time rewriting to clean up the LLM smell, so I'm unsure of what the future LLM-as-editor will be.
The big problem with the linked poll by Cynthia Dunlop is that it's all self-reported.
The fact that the sample is not representative of the general population rather but might be closer of 'early adopter'/'power users' is interesting.
But the idea that "I prefer authenticity to polished crowd-pleasing content" is something that people love to believe about themselves, but is hardly ever supported by facts.
As someone who spends a lot of time painting (maybe more time thinking about it than doing it, but still), it is quite evident that this is a fable. AI content is now everywhere in the streets -- just yesterday I went to a fair and food stands were divided into 2, the ones that hadn't updated their menu in 10 years or more, and the one that had generated it with ChatGPT. Museums are shameless at using AI images for their signs, and way too often even for their content. People do not prefer crappy human art, and those who self-report they do fail very hard at 'image Turing tests'.
I think the general point is true, but it does not give any timescale of when the dark age might end, when the tools will adapt etc.
The dream in itself has been destroyed.
The idea that you could just have a machine enumerate all valid theorems in a theory is part of it, but it's only a question of form.
The point was that it was to prove "all theorems of Mathematic", not "theorems into a given axiomatic system that is useful in some contexts, e.g. ZFC".
You could even argue that it's the fundamental basis for post-modernism, since mathematics have destroyed the notion of absolute truth in any advanced domain. It's back to a form of "all models are wrong but some are useful" similar to what we have in physics. Sayonara, Plato.
My first experience with a GUI was the HP-40G calculators. By their nature, they only have arrows and accept/cancel buttons.
It featured very advanced symbolic computation features (CAS that would step you through intermediary results), but the magical thing was how equations, rather than being a series of characters, that you piece up into meaningful chunks through parentheses, where actually displayed like mathematicians would write them.
Then, to select and edit a specific part of the equation, you have a natural 'box'; numerator/denominator, etc, then you can drill down into the recusirve structure of the mathematical expression. It also means that regular edits are 'correct' by default: delete a parenthesis and your expression is syntactically invalid, whereas "replace the numerator f(x)^2 by 6a" keep you in the space of syntactically valid expressions.
In other words, this is the holy trinity of UI: semantic - accessible - efficient
The experience is unparalleled to this day, although writing it down I realize more why it was never really reproduced.
For a browser, I would imagine having blocks like:
A. meta (browser itself) / B. page (DOM)
A1. page controls (bookmark, ...) / A2. Navigation experience (font size, dark mode, ...)
They bother with that effort when eating other things, but they keep it simple and go kraft-and-white-bread when making a grilled cheese. They're essentially saying, "While I love putting a lot of effort into cooking most things, when it comes to a grilled cheese, simple and cheap wins out."
They are feeding butter grass, they are way past the point of no return
/s
I think some things taste a lot better when you are so conscious about every ingredient and preparation. For sourdough and cheese I always prefer the good ones, what can I say.
>My biggest issue is that it’s impossible to engage with and give feedback on an AI written document, because it’s impossible to know whether misconceptions or gaps are because the author doesn’t understand the material deeply enough or the author does but the AI doesn’t and the author’s not proofreading carefully enough.
FWIW, same problem with PRs or PoC that I have to work on; now my first question is, "did you know about his behaviour?". The first step, getting a decent spec, is delayed to after a first draft implementation is already pushed...
FWIW, the only time I ever had emergency brakes kick in are in spurious situations, like tight maneuvers or there is something ahead with plenty of headway to decide whether you should brake or not. A cyclist moved close to the traffic light fast and the car completely stopped. This one was a bit more dangerous because had there been someone behind, that driver would not have expected such an abrupt stop.
>so I would get random brake slams which would panic me more
Every time it happens, it hurts as I'm not prepared for it.
Lane assist is also particularly bad as it handles some slight curves incorrectly, so it resists your driving. As a result with such cars I have my arms muscles tense up in anticipation of some turns.
Apparently my definition of tutor is so demanding that it should not be expected at all from a tutor (even if provided with information on the tutees weaknesses, tutors don't use the information effectively). However, the point of these studies are to gauge large scale effects rather than high variance small sample size effects. There's a lot more that is very interesting.
To me, what makes a game a game is that you can learn how it works simply by interacting with it; you don't need to open a separate wiki. That is not entirely true, as for examples fighting games have been infamous for needing to go online to learn how combos work, but this is widely considered to be a major factor of why the genre is unpopular, and recent games have tried to at least give proper tools (in training mode).
Right now, it feels a bit like a series of exercises with the guiding text replaced by dungeon fluff; it's pretty neat, yet you could as much say 'just give me the tutorial'.
In a game format I would for instance expect not to have to type the "proof [...] qed" part for example; its purpose is to be a bounding box, but interacting through text is cumbersome -- it isn't really for a developer who sees the benefit of plain text, but it is for a most users who might bang their head against the syntactic impedance mismatch.
To put that into perspective though, I remember Brett Victor's "Alligator Eggs", and the idea is very compelling; games are self-motivating, so if you can learn some real skills then you solved everything.
Combinatory logic, sequent calculi etc naturally lend themselves pretty well to the puzzle formats, yet I don't think there's anyone who really succeeded at any real implementation of it.
I'm mostly rambling my own view on the subject here, it's certainly an interesting experiment :-)
Yeah the game was thought to be an extension of the tutorial and an educational/grinding environment for the theory and the language.
About interacting with text, in that case I think it is exactly the opposite. The purpose is to be a funny shell around a bunch of exercises that would fell tedious (for me, at last) without it. It is meant to be a roguelike dungeon crawler about proof theory, so yeah, it is expected the player to learn to write proofs.
To me there are still 2 big problems
1. The language ergonomics. This is what I want to work on next.
2. The progression of the game levels and the tutorial. The goal is that they introduce the tool (algae), introduce proof techniques (ex: to proof a conditional you assume the premise and prove the conclusion) with some progression, and provide a playground through the game
The whole write-up is quite interesting so I'll definitely try it out.
reply