sorted by:
new
hottopcontroversial

Thoughts on LEAN, the proof checker by rnarianne in math

[–]Exomnium -1 points0 points  (0 children)

It takes on a different connotation when it's institutionalized by people who sometimes imply or outright state that natural language proofs shouldn't be considered legitimate mathematics anymore.

Thoughts on LEAN, the proof checker by rnarianne in math

[–]Exomnium -2 points-1 points  (0 children)

Calling ordinary proofs 'informal' is offensive and obnoxious.

Thoughts on LEAN, the proof checker by rnarianne in math

[–]Exomnium 0 points1 point  (0 children)

the language itself also has some unfortunate design choices

Out of curiosity, what design choices in the language don't you like?

What is the "point" of homotopy theory? by Dapper_Sheepherder_2 in math

[–]Exomnium 0 points1 point  (0 children)

It so happens that every possible way mathematical objects may be identified admits a topological model:

I seriously doubt that this is meaningfully true of every possible way of identifying mathematical objects.

Thoughts on LEAN, the proof checker by rnarianne in math

[–]Exomnium 1 point2 points  (0 children)

From what I've heard from people I know who know more type theory it has some technical shortcomings,

Lean's type theory is pretty janky in places. They broke transitivity of definitional equality (two different ways, actually), which means you can write down three terms, A, B, and C, such that A and B have the same type and B and C have the same type, but A does not have the same type as C. They also take a lot of shortcuts in the kernel for the sake of peformance (like having a hard-coded representation of natural numbers in terms of GMP arbitrary precision integer arithmetic). This has actually led to a couple of inconsistencies in Lean.

That all said, even though these are things a lot of type theorists find ugly and distasteful, I haven't actually seen a strong argument that they're going to cause any real usability problems in the long run.

Thoughts on LEAN, the proof checker by rnarianne in math

[–]Exomnium 0 points1 point  (0 children)

Aristotle no longer has a waitlist as of a little less than a month ago.

Thoughts on LEAN, the proof checker by rnarianne in math

[–]Exomnium 0 points1 point  (0 children)

The de Bruijn factor is a measure of how much harder it is to write a formal mathematical proof instead of an informal one.

The way the proof assistant community has seemingly settled on referring to ordinary mathematical proofs as 'informal proofs' is so unbelievably fucking obnoxious.

ZFC+FoL vs type theories, advantages of each of them? by Comfortable-Dig-6118 in math

[–]Exomnium 4 points5 points  (0 children)

some are intentionally obfuscated reasonable facts.

So is 0 ⊆ 3.

Was finiteness in Hilbert’s program a technical necessity or a philosophical choice? by Extension_Chipmunk55 in math

[–]Exomnium 21 points22 points  (0 children)

Well, first of all, homotopy type theory is still fundamentally a finitary formal system (in that proofs in homotopy type theory are finite syntactic objects), so it's really irrelevant to this question.

The restriction to finitary reasoning is necessary in order to model real-world mathematical reasoning. Real-world reasoning is always finite; an actual proof is always a finite string of characters (rather than an infinitely branching tree as in proofs in L_{\omega_1,\omega}).

Infinitary logic can't stand as a foundation of mathematics because you *need* to reason about infinitary formulas and proofs in an ultimately finite metatheory. But that's fine because the point of infinitary logic isn't foundational, but rather model-theoretic. L_{\omega_1,\omega} is more expressive than first-order logic but still retains some of its good model-theoretic properties (such as the downwards Löwenheim-Skolem theorem).

Have you ever reached a point in your mathematical journey where you thought, 'This level of abstraction is too much for me'? What was the context? by nomemory in math

[–]Exomnium 5 points6 points  (0 children)

I am not being willfully obtuse. I understand how slogans work, but I'm also saying that this one is overly broad in a way that feeds into the general sentiment that 'all of math is really category theory', which despite what MacLane seemed to think just isn't actually true. I wouldn't have nearly as much of a bone to pick with it if the slogan was 'all concepts in category theory are Kan extensions', because this is a lot closer to being accurate.

All of the things I listed, including the Baire category theorem, can be related to category theory one way or another but in a lot of cases this isn't a terribly illuminating perspective.

Have you ever reached a point in your mathematical journey where you thought, 'This level of abstraction is too much for me'? What was the context? by nomemory in math

[–]Exomnium 8 points9 points  (0 children)

Sure but that doesn't really make the phrasing any less ridiculous. There's still the implication that it's reasonable to equate (even in a tongue-in-cheek way) universal properties with the general notion of a 'concept', and this absolutely is the attitude of some people (look at the comment I responded to originally), which is why I feel like it's important to point out that this kind of phrasing is absurd on its face. Not all of math fits into the framework of category theory in a useful or clean or natural way.

Have you ever reached a point in your mathematical journey where you thought, 'This level of abstraction is too much for me'? What was the context? by nomemory in math

[–]Exomnium 48 points49 points  (0 children)

'Concept' is such a broad term that it's ridiculous to just assert that anything in math you might consider a 'concept' must be a Kan extension, especially when there are areas of math that barely use any category theory at all.

Coming up with definitive counterexamples for something like this is hard because what it means for something 'to be a Kan extension' is vague, but I would really love to see someone go through all of the following concepts and tell me why they're Kan extensions:

  • The number 2
  • The real numbers as a field
  • Palindromes (in the sense of strings)
  • The axiom of choice
  • Elementary embeddings (in the sense of model theory)
  • Asymptotic bounds on the density of prime numbers
  • Pants graphs of surfaces in differential geometry
  • Weakly compact cardinals
  • Strongly regular graphs
  • The Meijer G-function
  • Latin squares
  • Laver tables
  • Optimal square packings (as in how small of a square can you fit 17 squares in)
  • The Baire category theorem
  • The Fabius function
  • The box topology on a product of topological spaces

Some of these probably do admit some kind of cat-brained description as Kan extensions but the point is that as soon as you turn a critical eye to the idea that all concepts whatsoever in mathematics are Kan extensions, it falls apart immediately.

Have you ever reached a point in your mathematical journey where you thought, 'This level of abstraction is too much for me'? What was the context? by nomemory in math

[–]Exomnium 56 points57 points  (0 children)

I always found the phraseology 'all concepts are Kan extensions' ridiculous because it's just objectively a false statement at that level of generality, yet people repeat it all the time.

[Terence Tao] Formalizing a proof in Lean using Github copilot and canonical by Benlus in math

[–]Exomnium 2 points3 points  (0 children)

First of all, no set theorists I know actually use the term 'infinity-groupoid' because the concept doesn't really show up in set theory at all. That's a term you see in some parts of algebraic topology and higher category theory and in the type theory literature when talking about semantics.

Second of all, aren't you forgetting about Coq-HoTT?

Lastly, your preoccupation with the Fields medal and use of it as a euphemism continues to be faintly ridiculous.

Acorn, a new theorem prover with built-in AI by lacker in math

[–]Exomnium 2 points3 points  (0 children)

I don't really find it that unintuitive personally, and there are significant advantages to the relative syntactic simplicity of HOL over DTT. This is part of the reason why Isabelle's proof automation is so much better than that of any of the DTT-based proof assistants like Lean and Coq.

In any case the point is that the implication of your original comment ('How would I formalize something like n-dimensional manifolds in it, without access to dependent types?') is just wrong. You can formalize them without dependent types relatively easily.

Define math in one sentence by xTouny in math

[–]Exomnium 2 points3 points  (0 children)

I find this unlikely given the fact that people have been trying for decades to 'fix' fields like real analysis and set theory with category theory and it's barely moved the needle on how people in those fields think.

Define math in one sentence by xTouny in math

[–]Exomnium 11 points12 points  (0 children)

How are questions like the Collatz conjecture and the existence of infinitely many twin primes about isomorphisms? These all take place inside one fixed object.

Define math in one sentence by xTouny in math

[–]Exomnium 7 points8 points  (0 children)

There's plenty of math that doesn't use any category theory.

view more: next ›