@boarders@mathstodon.xyz
@boarders@mathstodon.xyz avatar

boarders

@boarders@mathstodon.xyz

Interested in mathematics (homotopy theory, category theory, topos theory), programming languages and philosophy

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

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

boarders,
@boarders@mathstodon.xyz avatar

The thing he emphasizes is different models and this I strongly agree with.

In ZFC, any vector space has a basis as a result of the AOC (axiom of choice). Debating whether every vector space has a basis by arguing about matching socks or Banach—Tarski is a waste of time from a bygone age. Instead, we should realize the mathematical fact that in a sheaf topos on a space X, if we consider a vector space then this is a continuous family of vector spaces on X and a choice of basis amounts to a global trivialization of the corresponding bundle. There exists non-trivial vector bundles however (in any kind of mathematics we choose!), and so we have reasons to not believe in the AOC.

boarders,
@boarders@mathstodon.xyz avatar

@codyroux it is like science - we fundamentally rely in scientific theorizing on epistemic norms (of beauty, simplicity, elegance, fallibility in the face of evidence etc.), and we should be loath to give up such virtues as essential to the scientific attitude given what they have given us so far

boarders,
@boarders@mathstodon.xyz avatar

@robinadams ah yes, a good point

boarders,
@boarders@mathstodon.xyz avatar

@robinadams I would still think it is better for me to think of this as meta-theoretic reasoning about ZFC in a model of ZFC

boarders,
@boarders@mathstodon.xyz avatar

@mudri still trying to think of the best way to think about this question

joey, to random
@joey@mathstodon.xyz avatar

I think I asked this before but:

Is there an analog of "locality" when moving from topological spaces sheaves to sheaves on a site? Or was it something specific to spaces that was generalized away when moving to sites?

boarders,
@boarders@mathstodon.xyz avatar

@joey what does locality mean for spaces?

antidote, to random
@antidote@mathstodon.xyz avatar

Can someone give me a really good excuse to learn (algebraic) geometry? As an outsider, the maths sounds like a real challenge and something I’d probably get a lot out of learning, but I’ve not got any real motivations to step on the ladder!

boarders,
@boarders@mathstodon.xyz avatar

@antidote start out with the Weil conjectures - they say that if you have a curve/higher dim analog over a finite field, then you can count the number of points by considering the cohomology of the corresponding subset in the complex numbers! It is really one of the most incredible facts that this works out. See these notes for the best intro: http://www.stat.ucla.edu/~ywu/wbook.pdf

deech, to random
@deech@mastodon.social avatar

Git reflog should be taught on day 0. It is the easiest way of getting out of jams which is basically your life with Git.

boarders,
@boarders@mathstodon.xyz avatar

@deech it’s like climbing, learn what to do when you fall first

pkhuong, to random

Work is both performance and liability^Wcorrectness oriented, and I noticed a common pattern is that we'll generate commands with a fully deterministic program (i.e., a function), reify the command stream, and act on the commands.The IO monad is real!

boarders,
@boarders@mathstodon.xyz avatar

@pkhuong the spirit of lisp lives on

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.

boarders,
@boarders@mathstodon.xyz avatar

@codyroux the converse is more than fair though, solving constraint satisfaction problems by hand is not my idea of fun, but the idea you can mechanize it is

typeswitch, to random
@typeswitch@gamedev.lgbt avatar

C library functions are always like: "SYNOPISIS. This function converts foos into bars depending on the user locale. ARGUMENTS. src and dest pointers must be distinct; it is undefined behavior if they are not QPU-aligned. RETURN VALUE. Returns the number of foos converted. A zero value indicates failure, or that zero foos were converted. A negative value indicates that the final foo was only partially converted (function got tired). Check errno global to find out why."

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

@typeswitch it sounds bad BUT you can target this code to not work on multiple platforms in multiple distinct ways

highergeometer, to random
@highergeometer@mathstodon.xyz avatar

If you had to prove there were no square circles, how would you go about it? And state your context and assumptions/definitions up front.

boarders,
@boarders@mathstodon.xyz avatar

@highergeometer you can also study things like circles in the p-adics or ask about analogues of pi (which I believe gets into some rather fancy p-adic analysis)

boarders,
@boarders@mathstodon.xyz avatar

@highergeometer it’s kind of a mythical topic as it pertains to p-adic geometry and gets you into very modern stuff like Fontaine theory

boarders, to random
@boarders@mathstodon.xyz avatar

We have a bot trained on Xi Jinping thought before we have one trained on Jon Sterling thought - why our world is in decay

cbaberle, to random
@cbaberle@mathstodon.xyz avatar

Illustration of how the (n+1)-simplex can be obtained from the n-simplex by freely adjoining a terminal object, for n up to 4:

boarders,
@boarders@mathstodon.xyz avatar

@cbaberle this follows from tte more general join formula:

Δ[n]*Δ[m]=Δ[n+m+1]

boarders, to random
@boarders@mathstodon.xyz avatar

Rust + serde ecosystem is just way too good if you are writing anything that is mostly just data mangling against some known schema, no need to be using python for these tasks which makes me only ever regret the choice

roboguy, to random
@roboguy@mathstodon.xyz avatar

If we think of categories as being like "proof-relevant" preorders, then what is a "proof-relevant" locale?

I believe I've read that this is a topos. But how do we know that it has a subobject classifier? I see how it has finite products, arbitrary coproducts and exponentials.

boarders,
@boarders@mathstodon.xyz avatar

@roboguy don’t think just about generalizing the axioms of a locale - think about how it has a natural embedding in its powerset via the full downset and about the distinguished role played by downward closed sets in the theory

boarders,
@boarders@mathstodon.xyz avatar

@roboguy btw this is why @johncarlosbaez has this comment to the effect that decategorification is easy but categorification is an art

dmm, to random
@dmm@mathstodon.xyz avatar

Category theory friends: Is there a standard way to describe a functor?

I was using a two-case function to describe functor, where one case is what the functor does to objects and the other case is what the functor does to morphisms (see the image). However, I haven't been able to find a standard form in any of the literature I've been reading...

Thx, --dmm

boarders,
@boarders@mathstodon.xyz avatar

@dmm if F : C -> D, is a functor then people will overload the notation and define it by:

F A = A x S
F f = f x id

[notice here id is also overloaded since I don’t mention the type]

A less overloaded notation that is used quite a bit is to denote the object part by F_0 and the morphisms part by F_1:

F_0 A = A x S
F_1 f = f x id_S

mevenlennonbertrand, to random
@mevenlennonbertrand@lipn.info avatar

I just realised that inductively defining an indexed inductive family T : B -> Type and then quotienting each T x by a family of relations R : Π x : B, T x -> T x -> Type is not the same as the corresponding quotient inductive type: if R is not a congruence, then the quotient-after-the-fact is not right, because it does not know that you also want to quotient the other fibers by their relation.

Is this the whole point of QITs that had completely gone over my head until now?

boarders,
@boarders@mathstodon.xyz avatar

@mevenlennonbertrand yes! If you do raw syntax quotiented by beta/eta then that is not the same as the QIT with these equalities

boarders,
@boarders@mathstodon.xyz avatar

@jonmsterling @mevenlennonbertrand that is what I meant and actually I had in mind the situation of the syntactic category of a dep type theory where you must quotient all things together (contexts, types and terms) and you can’t add in congruence after the fact (maybe that’s technically wrong but adding it in after the fact is beyond brutal)

boarders, to random
@boarders@mathstodon.xyz avatar

I think “active learning”/“student-centred learning” and other new ideas for how university teaching might work are great. A model for learning based too much around “propositional knowledge” and too little around capacities and practices leaves us in the same decrepit situation as analytic philosophy’s view of epistemology (“justified true belief”). It is slightly sobering however that the gold standard of a “flipped classroom” is how high school mathematics works, and I don’t think many people would view that as any kind of ideal of education, to say the least

ltratt, to random
@ltratt@mastodon.social avatar

One thing I think about a lot is "how much time should this organisation spend making tools to help with its main software tasks?" Experience has taught me that most invest far too little in this, but I've struggled to find a good way of defining what "too much" might look like.

boarders,
@boarders@mathstodon.xyz avatar

@ltratt in the context of CI then I would say too much is indicative of situation where CI is far too slow and has enough false positives to create distrust

boarders, to random
@boarders@mathstodon.xyz avatar

https://www.experimental-history.com/p/how-to-get-7th-graders-to-smoke

"You cannot plonk someone in front of a computer screen for an hour and expect them to become a better person. Well-meaning researchers have tried way, way harder than that and gotten way, way less."

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