Post by Mild ShockTerence Tao, "Machine Assisted Proof"
http://youtu.be/AayZuuDDKP0
So, "Lean is the new concept-script Begriff"?
Mizar, Metamath, I suppose it was Mizar, and Z,
that was going to "canonize a formal library
of derivation methods and associated results".
https://en.wikipedia.org/wiki/Mizar_system
"Mizar: Since 1973...."
Many type inference systems, ....
"Classical" logic is "quasi-modal", ..., usually,
"classical quasi-modal logic".
https://en.wikipedia.org/wiki/Category:Large-scale_mathematical_formalization_projects
https://en.wikipedia.org/wiki/Category:Formal_systems
It seems like a reasonable sort of system,
just, enumerates logical antinomies, then
each of what results the principal branches
of the singularities either way, makes little theories,
with their limits and their incompleteness.
An example of this is ZF as it's usually considered.
The real issue for mathematics is getting to
where the types, for completions, are in effect
and actual, because, it's a real role for foundations.
Or as he put it, "trusting the compiler".
Isoperimetric theorems and packing problems,
they're pretty related. Basically looking for
when the angle of the packing and packed are
same, given arbitrary configurations around, ....
It seems like "New value of computer assistance?
More like the entire field is already based on it."
When they started pushing calculators in school,
it was like, I'm going to need trig and 1/x and
this fractional powers button is great, also e.
The rest of the graphing was like "no, thanks,
school already taught me".
So, Kepler conjecture, sphere-packing, seems for
a sort of equi-partitioning and equi-packing sort
of approach, for the isoperimetric, the isopacked.
Then he gets into Faltings purity and it's like
the only reason we're talking about Faltings purity
is because Scholze is dirty.
"This theorem is essential...", euh, here this is
the usual difference between "not.need T" and "need not.T",
Homotopy Type Theory is the strength of ZFC plus
two large cardinals, ..., it adds unvalency. Well, sure,
it's not consistent anymore, but it is more complete.
It's like a new math lib was announced, "you're right".
Freiman-Rusza conjecture, looks interesting,
it's in doubling-spaces.
Old wrapped as new, ....
I'm a fan, and kind of demand, Faltings purity.
For cross-checking compilers is "a little language
with a term re-write system that results Mizar, Metamath,
Coq, Lean, lambda calculus, category theory, descriptive
set theory, ....".