tlringer

10 ms·

31.
by tlringer 6y ago
Students under abusive advisors like this should not be punished and in fact are currently not punished. The power structures are too fundamental. The problem is that if you cross your advisor, good luck getting a job later.
32.
by tlringer 6y ago
If any one of his current students are reading this, feel free to reach out to me (use ringertalia@gmail.com), and I will help you find resources that may help you while prioritizing your safety. I recommend doing this from a non-university
33.
by tlringer 6y ago
Things to consider: 1. When under an abuser, frequently you internalize their narrative. 2. Allegedly the professor threatened to kill him if he "ruined his reputation." 3. If he was an international student (I do not know if he w
34.
by tlringer 6y ago
Someone really, really, really needs to get this professor's current students to safety immediately. Don't forget that shortly before the student's suicide, according to a screenshot of a conversation with the student who too
35.
by tlringer 6y ago
Finally, an excuse to nap
36.
by tlringer 6y ago
I'm really happy with the framing of this article, and with the nuance in discussing other ITPs and the history of ITPs!
37.
Proving Theorems with Computers (AMS Notice, Kevin Buzzard) [pdf](ams.org)
3 points by tlringer 6y ago|1 comments
38.
by tlringer 6y ago
I'm a woman though, and women rarely get positive attention for anything in CS. I'm bold because as a woman in the field you need to be bold to survive as a researcher. In the type theory and proof assistant worlds there are only
39.
by tlringer 6y ago
I have learned more about Kevin and feel bad for bringing up the heckling thing now. I would ignore that part of what I said.
40.
by tlringer 6y ago
It is my understanding that functional extensionality in Lean itself follows from the axiom propositional extensionality, so in that sense LEM is still a consequence of an axiom. The core theory of Lean is constructive.
41.
by tlringer 6y ago
That makes sense! I just wish discussion on this end would stay nuanced: In that case Lean has great library support for classical mathematics. This is an important distinction because it is something that the authors of other constructive
42.
by tlringer 6y ago
I like these lecture notes: https://staff.math.su.se/anders.mortberg/papers/cubicalmetho... But if that is too hard to read, I recommend telling Anders directly when you get confused. He is open to improving the n
43.
by tlringer 6y ago
Lean is not classical. I don't know where the idea that Lean is classical is coming from. Lean is constructive. It is consistent with classical axioms, just like Coq is, and just like Cubical is in the propositional fragment. Isabelle&
44.
by tlringer 6y ago
Lean isn't classical. Lean is the calculus of inductive constructions with uniqueness of identity proofs. Classical logic in Lean requires using axioms.
45.
by tlringer 6y ago
It does. And if classical logic is what they like, they can use Isabelle/HOL just as nicely. It is classical. It has wonderful automation. Kevin gets attention because he is bold, not because he is correct. Anonymous comments are cowar
46.
by tlringer 6y ago
There is RedPRL, there is also cubical Agda. I think cubical Agda is the best developed so far. It lacks automation. But that is not fundamental, it is thanks to the philosophies of the people involved. Lean is not weak, it just commits to
47.
by tlringer 6y ago
The idea of Lean being suitable for all of math is sensationalist and Kevin knows it. Lean being committed to UIP already rules out many kinds of mathematics. Furthermore, the kind of automation possible in Lean is also possible in univalen
48.
by tlringer 6y ago
If he means there was a time "before" time, wouldn't we need some metatheoretical notion of time to even state that? Like how can we state that in our system if our time begins at the big bang? I don't get it
49.
by tlringer 6y ago
Forgive my ignorance, but what does it mean for something to exist before the big bang? What happens to time at the boundaries?
50.
by tlringer 7y ago
Probably much less. It is not just running form that makes elite runners efficient. Due to both genetics and training, their bodies use fuel more efficiently, too.
51.
by tlringer 7y ago
Elite runners tend to burn much less than normal runners over the same distance, since they are typically lighter and more efficient. This race didn't follow the rules so he could do whatever he wanted. Under official rules, you can ha
52.
by tlringer 7y ago
The Nike shoes are legal, though controversial. Give it a few more years of further improvements to the shoe technology, and they will probably be banned and asterisks will be placed next to every record, like in swimming when technology go
53.
by tlringer 7y ago
That is all of LetsRun. It is an incredibly toxic community full of experts and trolls.
54.
by tlringer 7y ago
For one, pacemakers have to enter the race and start the race with him. You can't have pacemakers enter partway. They all have to be eligible to hit the record too if they are capable. Per IAAF rules, pacemakers are basically just comp
55.
by tlringer 7y ago
This is a really interesting idea. In some sense, you can say a proof script is "almost correct" if it proves a slightly different theorem. I suspect the one difficulty there would be finding such incremental changes on Github. It
56.
by tlringer 7y ago
That's a neat idea. It would mostly help for gathering data from beginners, which would be very skewed, but I'm sure it could still be useful, especially for developing tools to help beginners.
57.
by tlringer 7y ago
As an example of using semantic information, you might define a bunch of functions that take two natural numbers and return some result. Then you might write some proofs about those functions. Let's say you write those proofs via induc
58.
by tlringer 7y ago
There has been a lot of work like this popping up in the past year. I think it's somewhat promising, but for ML for ITPs to really become useful, I think the models need to better take into account semantic information about terms and
59.
by tlringer 7y ago
I developed a huge crush on a very close friend shortly after my ex broke up with me. He caught on and told me he wasn't interested. We are even better friends now than we were then. We just took a few weeks apart and then resumed. I a
60.
by tlringer 7y ago
How do we gather divorce statistics? Because divorce is an extreme case of what you mention, and a very common one.

More ›