2,521 karma · joined January 11, 2016
Every single company putting ads up in public is held to a higher standard.
How many Gigabytes would that be, compressed? Wikipedia once fit on a DVD
This might also allow for some interesting meta-mathematics
DrBecky's video on it: https://youtube.com/watch?v=z2JIkAPcdnU
- is incapable of apologizing
- has a history of abusive behavior
- doesn't have a sense of humor, especially at their own expense
"How to spot an idiot": https://youtube.com/watch?v=i2Lo8ChhOKU
Zuckerberg: Dumb fucks
Playlist showcasing the current restoration work: https://youtube.com/playlist?list=PLtpOUadaBh31n6Pdscwhwopmh...
If you provide tools that help an organization kill easier, and possibly lazily rely on your inaccurate tools' judgment, and you do not care about the outcomes of these tools' uses, that's on your soul, too.
Yes, causality and attribution are hard sometimes, but it may have been that without it, hundreds of humans would be alive right now, and he doesn't even know. Maybe he should talk to the kids' parents about what alignment means.
https://arstechnica.com/gadgets/2015/10/imax-with-laser-supe... mentions that with IMAX Laser:
> Colour-wise, the full Rec. 2020 gamut/space is available—though we weren’t shown any films/trailers that actually made use of this larger colour space; they all used the DCI’s standard P3 colour space.
https://en.wikipedia.org/wiki/Rec._2020
I have no idea how well the analog film compares there
https://moultano.wordpress.com/2026/06/19/where-to-find-the-...
Similarly, for Metamath Zero, MM1 compiles down to the MM0 base language: https://www.youtube.com/watch?v=A7WfrW7-ifw
I think it's just a neat example that helps one understand how the verifier itself works at the most fundamental level.
$c wff $. $( we use this $constant as a type of formula (well formed formula) $)
$c ( ) ! -> $. $( brackets, negation, implication $)
$v A B C $. $( $variables to be used in formulas $)
wa $f wff A $. $( $floating hypothesis "wa" which says, that A is a well-formed formula $)
wb $f wff B $.
wc $f wff C $.
$( The following assertions define the rules to create formulas $)
$( In Metamath (unlike Metamath Zero), definitions also use the $axiom statement type $)
wng $a wff ! A $. $( "not A is a well-formed-formula" - mandatory hypotheses are (wa) $)
wim $a wff ( A -> B ) $. $( "A implies B is a well-formed-formula" - mandatory hypotheses are (wa, wb) $)
$c |- $. $( this $constant will be used as a type of provable formula $)
$( Schemes of $axioms of propositional logic $)
a1 $a |- ( A -> ( B -> A ) ) $.
a2 $a |- ( ( A -> ( B -> C ) ) -> ( ( A -> B ) -> ( A -> C ) ) ) $.
a3 $a |- ( ( ! A -> ! B ) -> ( B -> A ) ) $.
$( Definition of the Modus Ponens rule of inference in new scope; otherwise $essential hypotheses (inputs) mp1, mp2 will become mandatory for all upcoming assertions $)
${
mp1 $e |- A $.
mp2 $e |- ( A -> B ) $.
mp $a |- B $. $( mandatory hypotheses of "mp" are (wa, wb, mp1, mp2) $)
$}
$( A $proof states the string of symbols to be proven, followed by a list of labels used by the stack machine $)
$( $floating and $essential hypotheses are pushed onto the top of the stack, $axioms and $proofs transform it by using the top of the stack as inputs $)
$( When the stack is empty at the end, the proof is successful, and the proved statement can be reused in further proofs using its label $)
$( " A implies ( B implies C) is a well-formed-formula" $)
formula1 $p wff ( A -> ( B -> C ) ) $= wa wb wc wim wim $.
$( "( A -> A ) -> ( A -> A ) is true (follows from the axioms)" $)
formula2 $p |- ( ( A -> A ) -> ( A -> A ) ) $= wa wa wa wim wim
wa wa wim wa wa wim wim
wa wa a1
wa wa wa a2
mp $.Metamath Zero's Haskell implementation 700, and the C implementation 1000 lines (or 1800 overall) https://github.com/digama0/mm0
How do other proof systems compare?
Some bug counts: https://tristan.st/blog/in_search_of_falsehood