1,280 karma · joined October 20, 2010
Seems working as intended? I’ve used a bank and Starbucks chatbots for customer service. Both times they seem so rudimentary and bad that it seemed anything could’ve been better, no LLM required. It took so much effort to get thru to a human.
I have to believe it was designed that way, to fob off as many as possible.
> The package, offering up to $20,000 is comprised of $10,000 in relocation cash, PLUS up to $10,000, dollar for dollar match, for approved renovations on an existing home, OR for a down payment on a newly constructed home within City limits.
Not “A $10k stipend is available for anyone moving to Cumberland, MD” as the submission title says currently , which sounded like a basic income.
I only mention this because I think my other comment confused the issue.
My other comment says there was a previous discussion but that was actually a 2020 comment to a different unrelated submission that was the only mention to the TTA that I could find on HN.
It was not a previous discussion of the submission here.
To help start a discussion though…
The TTA here refers to a series of books from my childhood with beautiful space ship art. Took me forever to find it recently.
It’s made it past the House but not the senate yet. [0]
What’s strange is “Effectively, this rule change [initial Section 174 amendment] was designed to encourage enterprises to shift software development activities and the related expenses to the US due to the more favorable tax treatment.” [1]
But seems outsourcing to outside-US has only increased?
[0]: https://www.congress.gov/bill/118th-congress/house-bill/7024
[1]: https://www.corumgroup.com/insights/major-tax-changes-us-sof...
What's interesting is the subtle shift from saying objective ability can improve to asking if schools can encourage (motivate?) students to engage.
I'm guessing most teachers know that given the right circumstance, students can be made to improve in math/reading. But getting all/most students to engaged in the right "kind of effortful study" is just a different task.
Is it possible that maybe Kasparov noticed and just like you, he went with it instead of making the hosts look bad?
“Tarski was a mathematician” is true if and only if Tarski was a mathematician. [1]
"Yes" and secondly "no". Here's two different RC algorithms with cycle collection without tracing:
1. Concurrent Cycle Collection in Reference Counted Systems (Bacon & Rajan. 2001) [1]. Note it has no "global tracing" - which is what's meant by "tracing" in popular usage (right?).
2. Trial deletion, like as actually usable in Nim with "--gc:orc" [2].
If the definition of GC encompassing RC has fallen out of favour in popular usage, it's not because of RC having or not having these two particular properties.
[1]: https://pages.cs.wisc.edu/~cymen/misc/interests/Bacon01Concu...
It's because algebraic type problems are typically of the form "Prove algebraic equation E", where E is relatively easy to translate into Lean language.
Whereas combinatoric problem types are of the form "Prove some open-ended expression P" that even if translated into Lean, it's not clear where to start to connect it to axioms or the eventual problem solution.
If that’s an okay way to describe it, then AlphaProof’s language model, likely trained only on Lean statements (?), would have a tough time generating plausible next steps to combinatorial problems for MCTS to explore?
That doesn’t mean the LM + MCTS architecture is bad though. It means the language model needs to be better at generating plausible next steps (sequence of tokens) with maybe a less axiomatic approach to evaluating the fitness of that step (less Lean reliance?).
Anyone know any details?
> The smartphone and cloud revolutions coincided almost perfectly with when interest rates fell to zero and then stayed in the deep freeze for a decade
> These developments gave VCs even more reason to invest in startups
> - New categories of mobile-first startups were around, with potential
Free money (ZIRP) fuelled investments, sure, yes, of course.
An interesting idea here is that the free money was sent into certain directions because certain foundational tech was already there: cloud (AWS, GCP, Azure) and mobile devices (iPhone, Android).
Even if money weren't free at the time, maybe the available money would've been sent to those (types of) startups anyway? Maybe tech history would've been the same, only slower?
> Hyponatremia occurs in a substantial fraction of nonelite marathon runners and can be severe.
> As marathon running has surged in popularity during the past quarter-century, reports have emerged of serious illness and death from hyponatremia, as in the case of a 28-year-old woman who died after the 2002 Boston Marathon.
> Participants in the 2002 Boston Marathon were recruited … 488 runners (64 percent) provided a usable blood sample at the finish line. Thirteen percent had hyponatremia (a serum sodium concentration of 135 mmol per liter or less); 0.6 percent had critical hyponatremia (120 mmol per liter or less).
[1]: Hyponatremia among Runners in the Boston Marathon. https://www.nejm.org/doi/full/10.1056/NEJMoa043901
Except in Saskatchewan and Alberta [1].
[1]: https://financialpost.com/personal-finance/mortgages-real-es...
Wouldn’t the grammar of errors have to also be LR? Doesn’t that limit the kind of errors you can report?
The article says the Minotaur myth’s labyrinth was “obviously a maze”, but I doubt it.
In the myth, Ariadne gave Theseus a ball of thread (a clew) on the advice of Daedalus, the creator of the labyrinth [1]. And “Theseus followed Daedalus' instructions given to Ariadne: go forwards, always down, and never left or right” [3] "till he found the Minotaur asleep in the inmost recess" [2].
Getting a "clew" instead of a map from the labyrinth's creator makes me think it's likely symbolic... or that Daedalus expected Theseus to do a DFS search? Plus the “clew” wasn't strictly needed, since reversing those instructions for finding the Minotaur would've got him out again.
That makes me think the Minotaur was trapped in a proper single-path labyrinth.
Of course it’s just interpretation, and some think differently [4], which makes this way more interesting!
[1]: https://en.wikipedia.org/wiki/Theseus#Theseus_and_the_Minota...
[2]: http://www.perseus.tufts.edu/hopper/text?doc=Perseus:text:19...
[3]: https://www.hellenic.org.au/post/theseus-and-the-minotaur-th...
[4]: Like here: https://en.wikipedia.org/wiki/Labyrinth#cite_ref-5 . But note the book it cites, from my reading of it, actually says something more nuanced and subject to interpretation.
Download is here? https://ecma-international.org/publications-and-standards/st...
MS made it open because...
> More than a year after being asked by the European Union to standardize their Office 2003 XML formats, Microsoft submitted 2,000 pages of documentation for a new file format to the Ecma International consortium for it to be made into an open standard. [1]
The competing OpenDocument Format was standardized first though [2].
[1]: https://en.wikipedia.org/wiki/Standardization_of_Office_Open...
I think a challenge with the simulated-is-real math/calculator argument is that the simulation operates syntactically thru derivation without meaning.
E.g. a simulation of ZF set theory cannot tell you the truth value of the Axiom of Choice - because it’s independent of the ZF axioms (it is undecidable in the Gödel incompleteness sense).
But “Although originally controversial, the axiom of choice is now used without reservation by most mathematicians” [1] - I guess it’s truth is self-evident semantically.
So because of incompleteness, simulated math/calc will always be “missing” something.
Of course a LLM will happily say A of C is true (or not) but is it just parroting from the dataset or hallucinating?
'XZ backdoor: "It's RCE, not auth bypass, and gated/unreplayable."' [0].
[0]: https://news.ycombinator.com/item?id=39877267 (811 comments)
- Android devices which needed the cross-sign compatibility dropped to 6.1%.
- “dropping the cross-sign will reduce the number of certificate bytes sent in a TLS handshake by over 40%.”
- “it will significantly reduce our operating costs”
Too bad for those who use their old Android devices to access the public library and can’t afford to upgrade.
It’s not ideal, but using Firefox Mobile to access Libby web app should still work?
> beginning April 15, 2024, Android 7.1.1 will be the earliest supported Android OS for all OverDrive apps and websites, including Libby.
This change was already delayed from 3 years ago as Let’s Encrypt found a workaround back then [1]. Too bad they aren’t delaying it anymore. Good bye to my old tablet for library ebooks.
[1]: https://android.stackexchange.com/questions/231025/lets-encr...
> Google Authenticator started syncing secrets to the cloud[0] which means that those secrets can now be accessed in new ways outside of the user's control[1], which resulted in a huge breach at a startup called Retool[2].
Retool points out the "attacker was able to navigate through multiple layers of security" [0], i.e.:
1. "through a SMS-based phishing attack" on "Several employees"
2. "one employee logged into the [SMS phishing] link", "logging into the fake portal"
3. "attacker called the [phished] employee" "and deepfaked our [IT team] employee’s actual voice"
4. "the [phished] employee grew more and more suspicious, but unfortunately did provide the attacker one ... (MFA) code" (over the call)
5. "The additional OTP token shared over the call was critical, because it allowed the attacker to add their own personal device to the employee’s Okta account, which allowed them to produce their own Okta MFA from that point forward."
6. "This enabled them to have an active GSuite session on that device." With "Google Authenticator synchronization feature that syncs MFA codes to the cloud", "if your Google account is compromised, so now are your MFA codes".
By #5, I'm thinking GA sync is about as blameworthy as Okta for allowing a device to be added with just a single additional OTP token shared over a phone call?
Here's a different perspective (tptacek) [1]:
>> We use OTPs extensively at Retool: it’s how we authenticate into [Google, Okta, internal VPN and Retool]
> They should stop using OTPs. OTPs are obsolete. For the past decade, the industry has been migrating from OTPs to phishing-proof authenticators: U2F, then WebAuthn, and now Passkeys†. The entire motivation for these new 2FA schemes is that OTPs are susceptible to phishing, and it is practically impossible to prevent phishing attacks with real user populations
> TOTP is dead. SMS is whatever "past dead" is. Whatever your system of record is for authentication (Okta, Google, what have you), it needs to require phishing-resistant authentication.
> My only concern is the present tense in this post about OTPs, and the diagnosis of the problem this post reached. The problem here isn't software custody of secrets. It's authenticators that only authenticate one way, from the user to the service.
The SOURCE property is optional and apparently more aspirational than real.
https://stackoverflow.com/questions/57380771/how-to-use-sour...
> Randall hypothesizes a plane of dark matter exists roughly on the plane of the Milky Way galaxy. As the Sun oscillates in its orbit around the center of the galaxy, it passes through the dark matter.