voxl

5 ms·

1.
by voxl 9d ago
You expect an arxiv only paper to be cited? Do you even know fuck all about scientific research? Do you think someone can slap "Foundations of" in an arxiv title and we are mandated to cite it?
2.
by voxl 9d ago
Your claim is still rubissh, as you neglected to interact with the rest of my comment: economic utility does not necessitate all mathematical output directly contributes. You redefine "forgot" to make it falsiable, but also neglec
3.
by voxl 9d ago
You bemoan the cherry picked example and counter with an unfalsifiable claim. Certainly we have remembered much more math than Calculus, and much of it has been of practical use. How can we hope to quantity the expenditure on math we'v
4.
by voxl 14d ago
Whataboutism. Two evils are still evil.
5.
by voxl 18d ago
Probably yes. Only a handful of mathematicians work on this particular problem, and ALL of them do not exclusively work on this problem, while having administrative and teaching duties. The real issue is we'll never know. The rich are
6.
by voxl 19d ago
No you see people that use AI generally don't bother to consider this unimportant detail. Or they ask the AI to "double check" its work.
7.
by voxl 20d ago
??? Look at any conference that publishes mechanized results? You'll see plenty of Isabelle, ACL2, Rocq, Agda. You exist in the pop science bubble. If Lean has done anything it's advertised itself well. It did a good job of that a
8.
by voxl 22d ago
It's a great comedy that we move the buck from "I don't trust the human proof" to "I don't trust the Lean proof" despite the level of trust dramatically increasing. Moving to HOL-light might be another mod
9.
by voxl 22d ago
Hearing someone say "the future of proofs is Lean" is a bit like hearing someone say "the future of programming is Rust." Sorry to disappoint, or happy to inform, there are hundreds of programming languages actively bein
10.
by voxl 24d ago
Missing information is different from paying the person who steals information instead of paying the person that produces it. Did you bother to think critically before you replied, or is an AI doing all your thinking as well?
11.
by voxl 24d ago
So you'd rather give money to the company that stole the copyrighted material of experts and academics instead of giving them money? Sure some textbooks are corporate greed schemes themselves, but many others are just the work of a gro
12.
by voxl 1mo ago
You mean that technology that resulted in a massive bubble, wasn't marketed as replacing all labor and giving the rich personal slaves? You mean the technology that enables human communication and creativity instead of promoting human
13.
by voxl 1mo ago
Horseshit. ~30% of US citizens are happy with this state of affairs. ~30% are completely disengaged, believe ridiculous things like "both sides are the same" or feel like politics doesn't effect them. ~30% voted for Harris, B
14.
by voxl 1mo ago
The software is heavily regulated for medical devices. Saying an MRI machine has bad software seems highly unlikely to me. This is of course different from Epic, but even then as a patient MyChart is really not that bad
15.
by voxl 1mo ago
Don't bother, Republicans are the only ones that care about the debt and their ideology makes them incapable of realizing there very choice of candidates is the exact problem
16.
by voxl 2mo ago
This is not the argument. It's not a comparison to gambling but a comparison to something that does not materially improve a person's life. Economic expenditure does not equate to human benefit. This is the original argument, and
17.
by voxl 2mo ago
Incorrect. The statement in Lean can itself be wrong. Moreover, they could be exploiting a kernel bug in Lean, of which we had one published literally a week ago.
18.
by voxl 2mo ago
What is absurd is evaluating something on the lines of code it produces. AI psychosis at work.
19.
by voxl 2mo ago
This is horseshit. Mathlib3 and mathlib4 all existed prior to LLMs. Unimath of Agda, mathematical components of Rocq, the list goes on. LLMs have done nothing for "making large scale mechanization viable." They have been viable. T
20.
by voxl 2mo ago
A basic course in statistics will inform you of why a 99.99% accurate test should be looked at with skepticism when diagnosing a rare disease. Yet we see the fancy 9s and think somehow this many 9s is enough.
21.
by voxl 2mo ago
Sure if you're a rich slave owner.
22.
by voxl 3mo ago
They would just choose a different domain name, it's not that important and the previous years tend to forward link anyway.
23.
by voxl 3mo ago
Researchers _would_ leave in droves if they could. But it turns out the entire world doesn't actually care much for research. The US was actually unique in that regard.
24.
by voxl 3mo ago
Comparing it to the trolley problem is incorrect. COVID had real potential to kill you , even as a young person. At that point its a matter of risk assessment for yourself. Take a 2% chance of dying, a slightly higher chance of reduced qua
25.
by voxl 3mo ago
Let's take a moment to put the AI psychosis down and think through your comment: 1. AI is so good that you can get your game working to your vision in a matter of weeks without needing to depend on godot 2. Godot is making a mistake re
26.
by voxl 3mo ago
My eyes rolled so far back I'm blind
27.
by voxl 3mo ago
It's a good thing what random people thing is not taken a science these days, oh wait I guess science is on a historic decline as well. Maybe it's not climate chance, pseudo intellectualism, late stage capitalism, etc. Nah, it&#x2
28.
by voxl 3mo ago
You should know full well you need some method of determining if a student is competent enough to move on to the next class in whatever sequence. Perhaps universities are slacking on this front, but at a minimum a student who doesn't u
29.
by voxl 3mo ago
Citation needed, the last time a colleague engaged with the education college and supposed educators they looked at an induction proof with sheer bewilderment as if teaching this at all was impossible
30.
by voxl 3mo ago
Fun projection, there are three steam decks amongst my roommates, all three of them use is basically daily.

More ›