performance & efficiency Show more

R&D in big corp's Show more

Do you ever look at the Wikipedia pages for numbers? They're rather interesting. In a nerdy kind of way.
en.wikipedia.org/wiki/10,000

@amiloradovsky Computer checked proof aren't the Philosopher's Stone, but it seems like a change of quantity into quality. I think it's a much bigger deal than contemporary mathematicians are willing to accept, and future generations looking back will be astounded at the resistance.

What I would love to see, but probably won't happen in my lifetime, is type checking of allegories.

HoTT paper Show more

HoTT paper Show more

HoTT paper Show more

HoTT paper Show more

HoTT paper Show more

HoTT paper Show more

HoTT paper Show more

HoTT paper Show more

math meta Show more

math meta Show more

content thoughts Show more

In case you thought everything in academia (or even just PLT) is consistent (h/t @samth@twitter.com, slide by Guy Steele groups.csail.mit.edu/mac/users)

content thoughts Show more

@amiloradovsky @TheAspiringHacker Dump of my translated notes, in case there's anything interesting for either of you:

Notes on course from XR

Higher-Inductive Types

One particularly useful case of providing equality paths is modular integers:

Inductive Z4: Type :=
| O: Z4
| S: Z4 -> Z4
| mod4: S(S(S(S 0))) = 0.

The definition of pred for Z4 is more correct / less wierd
than with ordinary Coq:

Definition pred (n: Z4) :=
match n with
| O => S(S(S O))
| S m => m.

Q: What does a drowning analytic number theorist say? A: log-log, log-log, log-log ...

Show more
Mathstodon

A Mastodon instance for maths people. The kind of people who make \(\pi z^2 \times a\) jokes.

Use \( and \) for inline LaTeX, and \[ and \] for display mode.