Replying to
@dpiponi@mathstodon.xyz
@dpiponi@mathstodon.xyz Memorized my card number and I highly recommend
Remote
J Carr
@jac@types.pl
mastodon
4.7.0-alpha.2+glitch
I like using logic to do things it was never meant to do
You can refer to me as J. or as Jason
CS PhD student at UChicago
(all opinions my own)
0
Followers
0
Following
22
Posts
Joined December 23, 2025
Posts
Replying to
@markusde@mathstodon.xyz
@markusde@mathstodon.xyz I believe the successor function is undefined everywhere and there are no numbers greater than 0.
Replying to
@jonmsterling@mathstodon.xyz
@jonmsterling Such is the unfortunate consequence of sparking debate on Mastodon. At least there's no algorithm sharing it further for "engagement"
Replying to
@liamoc@types.pl
@liamoc
I don't understand what scenario you're referring to.
But in any case it's pure network and resourcing effects. I don't think there's reason to consider if one person asked. But if lots of people were using it I would not consider stubbornness to be worth the price.
Every new thing is bad until it is good.
@jonmsterling
Replying to
@liamoc@types.pl
@liamoc
Right so the analogue here is that people who write Rust spend more time worrying about memory safety and concurrency.
And that's true. Having a GC would be easier than worrying about where things are allocated.
But the other reason they spend more time thinking about it is that they want to think about allocating memory efficiently, and don't want to debug segfaults. And for them, Rust just works. Everything magically is memory-safe.
But if you don't want to write systems code, there's a wrong takeaway which is that Rust is therefore worse than C++, and a right takeaway which is that you're not interested in solving those sorts of problems.
But I think for your students, it goes back to my sentence that Nix sucks for one person. You get to solve everything yourself but not re-use the solutions. It also ultimately comes down to whether tools intend to support it.
@jonmsterling
Replying to
@liamoc@types.pl
@liamoc
Well that would be consistent with me saying factual things wouldn't it.
@jonmsterling
Replying to
@liamoc@types.pl
@liamoc
I think this is correlation rather than (or actually as well as) causation. I know someone of the sort, who uses Nix but not NixOS, but also really loves thinking about config. And tbh I've sometimes over-optimized.
I use NixOS because it "just works" and everything is remarkably easy to configure and doesn't randomly break. And I use Nix because we can guarantee pinned dependencies, and nonsense like patched LLVM (I'm sure they'll patch those crashes someday) and I don't have to keep track of some random dependency installed somewhere that might change.
I think there's a correlation in that if you use Nix(OS) it's significantly easier to try for insane setups and be able to manage the complexity. And people who like that also tend to be happy to explore new software.
Now it kinda sucks for one person, but with two it's great.
@jonmsterling
Replying to
@totbwf@types.pl
@totbwf
Tbh NixOS is great because any service you can imagine has a configuration option
services.foo.enable = true; which sets it up with perfect reasonable defaults. Every configuration you could want has a flag and you never have to know how to work with whatever random bespoke config format that your one specific service has (but you can if you want).
They always have an easy uninstall.
The difficult thing is running random binaries off the internet, but that's usually a thing that deserves a moment of thought anyway
Replying to
@androcat@toot.cat
@androcat@toot.cat Thanks for the response! I think there's still two counterarguments:
-
For informal proofs, RL prioritizes reasoning that appears valid, and I'm not sure how much they use things like known results
-
Tools like Lean both give feedback on valid proofs enabling systems to learn to produce them, and drastically reduce the checking surface (down to just the definitions).
Replying to
@koronkebitch@types.pl
@koronkebitch@types.pl @chrisamaphone@hci.social
Does this end at "Write up dissertation" because there's no step where you find a professorship 🙃?
Replying to
@androcat@toot.cat
I believe I already said what you said, as well as addressing why the reasoning is flawed, in my first message.
GenAI is indeed just a stochastic search tool over the space of relevant text, that is biased towards producing text which is a valid proof (via RL).
One should not mistake the methods for the outcomes.
Otherwise, I believe you're attacking an imaginary adversary here; nobody made any claim of understanding as far as I can tell. You then proceeded to jump into ad hominims, which I certainly don't appreciate.
I genuinely believe it is worth understanding the depth of theoretical math that goes into machine learning and AI, along with the extensive history of empirical science.
Replying to
@androcat@toot.cat
@androcat@toot.cat
Then I believe you are far out of date on your understanding and I would recommend you learn a bit about modern ML and AI methodology before commenting
@tao@mathstodon.xyz
Replying to
@androcat@toot.cat
@androcat@toot.cat
GenAI is indeed just a stochastic search tool over the space of relevant text, that is biased towards producing text which is a valid proof (via RL).
One should not mistake the methods for the outcomes.
@tao@mathstodon.xyz
Replying to
@totbwf@types.pl
@totbwf@types.pl Iirc this had to do more with a difference in uptime counting
Replying to
@jonmsterling@mathstodon.xyz
@jonmsterling I could see a sort of two-worlds claim that it's reasonable.
Namely, one may believe that truly everything is either true or false, that axiom of choice holds, etc, and yet still distinguish truth from the notion of construction. But under unique choice these must be the same.
One could of course *still* take the narrower choice that commutes \exists! and thus results in a proposition "there exists a unique function"
Replying to
@ncf@types.pl
@ncf I assume by relation you mean prop-valued. In that case decidability is effectively a prop (even without extensionality we can factor through its truncation)
strong total => decidable: so eliminate the truncation and we have inputs x y, and a function d: ∀ x y. (x ≤ y) + (y ≤ x). We play this function against itself:
consider d x y, and d y x. If the first returns the left branch or the latter returns the right, we're done by picking x ≤ y. But otherwise we have y ≤ x, in which case given x ≤ y we have x = x, and hence the two functions must have agreed, and hence we have a contradiction
strong total <= decidable: Given a decision d, and any inputs x y, let's prove x ≤ y + y ≤ x, Consider d x y, d y x. If Either returns their first input, we are done. But if both return the negation, we have a contradiction using totality, hence we have handled all cases.
Replying to
@mxchara@seattle.pink
Replying to
@foxy@blahaj.zone
@foxy 0) US
1) Funded up to 6 years, no masters required, masters can shorten requirements and funding by 1 year,
2) 9 classes under quarters, currently
3) 5-10hr/wk realistically
Replying to
@edwinb@types.pl
@edwinb They're keeping up with the times and using incorrectness logic to make a complete but unsound assertion.
Conditional on being malnourished/underweight, eating ice cream is good
Replying to
@koronkebitch@types.pl
@koronkebitch The existence of genAI for coding has brought me significant anguish. One of the things that was always a passion for me was the way that PL was fundamentally informed by human usability, education and communication. I have become somewhat more comfortable for the benefit of accessibility, but terrified of worsening connection between humans.
Replying to
@dysfun@social.treehouse.systems
@dysfun@social.treehouse.systems
Well Axiom f: False. is 15, but with work I'm sure we could bring it down
@treehouse.systems @jesper@agda.club @mevenlennonbertrand@lipn.info