@codyroux@mathstodon.xyz avatar

codyroux

@codyroux@mathstodon.xyz

Applied scientist at AWS. Proof theory enthusiast. Ultrafinitist.

This profile is from a federated server and may be incomplete. Browse more on the original instance.

codyroux, to random
@codyroux@mathstodon.xyz avatar

The amount of people claiming to hate math but love sudoku is alarming.

Reminds me of people who love poetry but hate rap.

codyroux,
@codyroux@mathstodon.xyz avatar

@boarders it's all just constraint satisfaction though :)

BTW I learned that a "true" sudoku must be solvable without backtracking.

boarders, (edited ) to random
@boarders@mathstodon.xyz avatar

Andrej Bauer gave an excellent recent talk “How to not believe in the law of excluded middle”: https://youtu.be/96iHUx0aGDs?si=y9j8Kc9znPs-cS1U

Towards the beginning he mentions some bad reasons for not believing in excluded middle include the undecidability of CH. This is true, but I don’t think it is a bad thing to mention (or perhaps I just feel bad since I am guilty of having done so) since:

  • CH ∨ ¬CH - “CH is either true or false” is a theorem of ZFC since it is just an instance of LEM. This is obviously not a solution to Hilbert’s first problem

  • Pr(CH) ∨ Pr(¬CH)- “there is a proof of CH or a proof of its negation in ZFC”. This is is not true, as shown by Cohen + Gödel (this is not an internal statement in ZFC, it is meta-theoretical)

  • Dec(Pr(CH)) - it is decidable that we can give a proof of CH, or that we can’t give a proof. This is also true, but this time we can’t appeal to LEM so we must be appealing to something else (in this case we appeal again to Cohen + Gödel). But this means we don’t accept the meta-theoretic principle LEM when it comes to statements about provability

codyroux,
@codyroux@mathstodon.xyz avatar

@boarders I think you'll find that a lot of math is only done because we're motivated by the aesthetics of the results.

Why not have similar motivations about foundations? It's not like Brower didn't know that you could prove certain things with choice or EM.

codyroux,
@codyroux@mathstodon.xyz avatar

@boarders yes, I don't know why failure of completeness shouldn't be taken seriously.

dpiponi, to random
@dpiponi@mathstodon.xyz avatar

Despite Wildberger being a bit off the usual conventional paths in mathematics, he's influenced me to the point where every time I write a line of code using an angle I ask myself if I could use an alternative "rational" representation.

https://research.unsw.edu.au/people/professor-norman-j-wildberger

codyroux,
@codyroux@mathstodon.xyz avatar

@johncarlosbaez @BartoszMilewski @dpiponi seems a bit harsh. Not sure you can avoid smell tests at the end of the day. Maybe you can try to ground them in things empirical, or theorems, but you're going to have to smell those as well.

codyroux,
@codyroux@mathstodon.xyz avatar

@johncarlosbaez @BartoszMilewski @dpiponi at the very least, though, ∀x, P(x) ⇒⊥ means that x-es such that P don't exist.

I feel like that's the common ground.

johncarlosbaez, to random
@johncarlosbaez@mathstodon.xyz avatar

Is there a chance that the physicist Oliver Heaviside was really Wolverine?

image/jpeg

codyroux,
@codyroux@mathstodon.xyz avatar

@johncarlosbaez surely he would rather be Magneto.

codyroux, to random
@codyroux@mathstodon.xyz avatar

Ideas for side projects? I'm very bored.

codyroux,
@codyroux@mathstodon.xyz avatar

@johncarlosbaez that's pretty good advice, thanks!

I do sometimes wish I'd stuck with those piano lessons as a kid.

gregeganSF, to random
@gregeganSF@mathstodon.xyz avatar

Wow, Thomas Hales and Koundinya Vajjha have proved Mahler’s First Conjecture! (That’s Kurt Mahler, not Gustave.)

https://arxiv.org/abs/2405.04331

Mahler’s First Conjecture says that the centrally symmetric convex shape with the worst possible packing ratio is made up of straight lines and arcs of hyperbolas, like the smoothed octagons shown in the animation below (demonstrating a 1-parameter family of slightly different packings all with the same density).

Whether these smoothed octagons are, as Karl Reinhardt conjectured, the actual worst case is still an open problem.

A bit more detail on Reinhardt’s conjecture in this article by @johncarlosbaez :

https://blogs.ams.org/visualinsight/2014/11/01/packing-smoothed-octagons/

and this thread by Koundinya Vajjha on Twitter:

https://twitter.com/KodyVajjha/status/1790211313618362848

A 1-parameter family of packings of smoothed octagons.

codyroux,
@codyroux@mathstodon.xyz avatar

@gregeganSF @johncarlosbaez packing conjectures are nuts (no pun intended)

codyroux, to random
@codyroux@mathstodon.xyz avatar

New episodes of the Church of Logic! We explain the basic idea behind ordinal analysis, one of the main mathematical/philosophical movements trying to justify logical laws.

With @sandmouth
https://podcasters.spotify.com/pod/show/cody-roux/episodes/The-Measure-of-Truth-Ordinal-Analysis-I-e2jc3as

codyroux,
@codyroux@mathstodon.xyz avatar

@brab @sandmouth Maybe you're asking for this? https://anchor.fm/s/db787130/podcast/rss

boarders, to random
@boarders@mathstodon.xyz avatar

What Scott calls the "first-order disease" - the absolute dominance of thinking the only truly worthwhile quantificational logics are first-order logics - has only confused me more over time. From a philosophical point of view only quantifying over "individuals" and the Quinian worry that quantifying over "properties" or "functions" represents a kind of platonism due to "ontological commitment" sounds like something from the scholastics and I am taken aback anyone takes it seriously. From a model theory point of view first-order logic is in some sense characterized by the Lowenheim--Skolem theorem and the compactness theorem (Lindström's theorem essentially says it is the strongest logic with these properties), guaranteeing both that it cannot prove categoricity results (so cannot hope to give any account of structuralism in mathematics), but also cannot talk directly about infinite or finite theories.

The most persistent version of this disease to me is the the intense focus in computability theory to think the only (partial) functions we care to discuss are those from ℕ → ℕ - bizarre that the failure of the higher-order Church--Turing thesis is not more widely studied

codyroux,
@codyroux@mathstodon.xyz avatar

@boarders at least in programming languages people think about defunctionalization, quote/eval, first class closures, first class continuations...

  • All
  • Subscribed
  • Moderated
  • Favorites
  • •
  • provamag3
  • rosin
  • InstantRegret
  • mdbf
  • osvaldo12
  • Durango
  • DreamBathrooms
  • everett
  • magazineikmin
  • thenastyranch
  • ngwrru68w68
  • Youngstown
  • slotface
  • kavyap
  • JUstTest
  • khanakhh
  • Leos
  • cisconetworking
  • tacticalgear
  • modclub
  • GTA5RPClips
  • cubers
  • ethstaker
  • anitta
  • megavids
  • normalnudes
  • tester
  • lostlight
  • All magazines
    •