**nhaliday + heavyweights**
61

Leslie Lamport: Thinking Above the Code - YouTube

heavyweights cs distributed systems system-design formal-methods rigor correctness rhetoric contrarianism presentation video detail-architecture engineering programming thinking writing technical-writing concurrency protocol-metadata

5 weeks ago by nhaliday

heavyweights cs distributed systems system-design formal-methods rigor correctness rhetoric contrarianism presentation video detail-architecture engineering programming thinking writing technical-writing concurrency protocol-metadata

5 weeks ago by nhaliday

big list - Are there proofs that you feel you did not "understand" for a long time? - MathOverflow

nibble q-n-a overflow soft-question big-list math proofs expert-experience heavyweights gowers mathtariat reflection learning intricacy grokkability intuition algebra math.GR motivation math.GN topology synthesis math.CT computation tcs logic iteration-recursion math.CA extrema smoothness span-cover

6 weeks ago by nhaliday

nibble q-n-a overflow soft-question big-list math proofs expert-experience heavyweights gowers mathtariat reflection learning intricacy grokkability intuition algebra math.GR motivation math.GN topology synthesis math.CT computation tcs logic iteration-recursion math.CA extrema smoothness span-cover

6 weeks ago by nhaliday

Epigrams in Programming | Computer Science

6 weeks ago by nhaliday

- Alan Perlis

nibble
quotes
aphorism
list
cs
computation
programming
pls
hi-order-bits
synthesis
lens
data-structures
arrows
algorithms
iteration-recursion
intricacy
strings
types
math
formal-methods
pic
visuo
visual-understanding
systems
state
structure
turing
cost-benefit
lisp
performance
software
language
plt
invariance
ends-means
ai
nitty-gritty
sci-comp
composition-decomposition
tradeoffs
grokkability
assembly
internet
egalitarianism-hierarchy
functional
impetus
roots
path-dependence
heavyweights
6 weeks ago by nhaliday

Zero-based numbering - Wikipedia

9 weeks ago by nhaliday

https://www.cs.utexas.edu/users/EWD/transcriptions/EWD08xx/EWD831.html

https://softwareengineering.stackexchange.com/questions/110804/why-are-zero-based-arrays-the-norm

idk about this guy's competence. he seems to want to sensationalize the historical reasons while ignoring or being ignorant of the legitimate mathematical reasons:

http://exple.tive.org/blarg/2013/10/22/citation-needed/

nibble
concept
wiki
reference
programming
pls
c(pp)
systems
plt
roots
explanans
degrees-of-freedom
data-structures
multi
hmm
debate
critique
ideas
techtariat
rant
q-n-a
stackex
compilers
performance
calculation
correctness
mental-math
parsimony
whole-partial-many
tradition
worse-is-better/the-right-thing
mit
business
rhetoric
worrydream
flux-stasis
legacy
elegance
stories
blowhards
idk
org:junk
intricacy
measure
debugging
best-practices
notation
heavyweights
protocol-metadata
https://softwareengineering.stackexchange.com/questions/110804/why-are-zero-based-arrays-the-norm

idk about this guy's competence. he seems to want to sensationalize the historical reasons while ignoring or being ignorant of the legitimate mathematical reasons:

http://exple.tive.org/blarg/2013/10/22/citation-needed/

9 weeks ago by nhaliday

The Existential Risk of Math Errors - Gwern.net

10 weeks ago by nhaliday

How big is this upper bound? Mathematicians have often made errors in proofs. But it’s rarer for ideas to be accepted for a long time and then rejected. But we can divide errors into 2 basic cases corresponding to type I and type II errors:

1. Mistakes where the theorem is still true, but the proof was incorrect (type I)

2. Mistakes where the theorem was false, and the proof was also necessarily incorrect (type II)

Before someone comes up with a final answer, a mathematician may have many levels of intuition in formulating & working on the problem, but we’ll consider the final end-product where the mathematician feels satisfied that he has solved it. Case 1 is perhaps the most common case, with innumerable examples; this is sometimes due to mistakes in the proof that anyone would accept is a mistake, but many of these cases are due to changing standards of proof. For example, when David Hilbert discovered errors in Euclid’s proofs which no one noticed before, the theorems were still true, and the gaps more due to Hilbert being a modern mathematician thinking in terms of formal systems (which of course Euclid did not think in). (David Hilbert himself turns out to be a useful example of the other kind of error: his famous list of 23 problems was accompanied by definite opinions on the outcome of each problem and sometimes timings, several of which were wrong or questionable5.) Similarly, early calculus used ‘infinitesimals’ which were sometimes treated as being 0 and sometimes treated as an indefinitely small non-zero number; this was incoherent and strictly speaking, practically all of the calculus results were wrong because they relied on an incoherent concept - but of course the results were some of the greatest mathematical work ever conducted6 and when later mathematicians put calculus on a more rigorous footing, they immediately re-derived those results (sometimes with important qualifications), and doubtless as modern math evolves other fields have sometimes needed to go back and clean up the foundations and will in the future.7

...

Isaac Newton, incidentally, gave two proofs of the same solution to a problem in probability, one via enumeration and the other more abstract; the enumeration was correct, but the other proof totally wrong and this was not noticed for a long time, leading Stigler to remark:

...

TYPE I > TYPE II?

“Lefschetz was a purely intuitive mathematician. It was said of him that he had never given a completely correct proof, but had never made a wrong guess either.”

- Gian-Carlo Rota13

Case 2 is disturbing, since it is a case in which we wind up with false beliefs and also false beliefs about our beliefs (we no longer know that we don’t know). Case 2 could lead to extinction.

...

Except, errors do not seem to be evenly & randomly distributed between case 1 and case 2. There seem to be far more case 1s than case 2s, as already mentioned in the early calculus example: far more than 50% of the early calculus results were correct when checked more rigorously. Richard Hamming attributes to Ralph Boas a comment that while editing Mathematical Reviews that “of the new results in the papers reviewed most are true but the corresponding proofs are perhaps half the time plain wrong”.

...

Gian-Carlo Rota gives us an example with Hilbert:

...

Olga labored for three years; it turned out that all mistakes could be corrected without any major changes in the statement of the theorems. There was one exception, a paper Hilbert wrote in his old age, which could not be fixed; it was a purported proof of the continuum hypothesis, you will find it in a volume of the Mathematische Annalen of the early thirties.

...

Leslie Lamport advocates for machine-checked proofs and a more rigorous style of proofs similar to natural deduction, noting a mathematician acquaintance guesses at a broad error rate of 1/329 and that he routinely found mistakes in his own proofs and, worse, believed false conjectures30.

[more on these "structured proofs":

https://academia.stackexchange.com/questions/52435/does-anyone-actually-publish-structured-proofs

https://mathoverflow.net/questions/35727/community-experiences-writing-lamports-structured-proofs

]

We can probably add software to that list: early software engineering work found that, dismayingly, bug rates seem to be simply a function of lines of code, and one would expect diseconomies of scale. So one would expect that in going from the ~4,000 lines of code of the Microsoft DOS operating system kernel to the ~50,000,000 lines of code in Windows Server 2003 (with full systems of applications and libraries being even larger: the comprehensive Debian repository in 2007 contained ~323,551,126 lines of code) that the number of active bugs at any time would be… fairly large. Mathematical software is hopefully better, but practitioners still run into issues (eg Durán et al 2014, Fonseca et al 2017) and I don’t know of any research pinning down how buggy key mathematical systems like Mathematica are or how much published mathematics may be erroneous due to bugs. This general problem led to predictions of doom and spurred much research into automated proof-checking, static analysis, and functional languages31.

[related:

https://mathoverflow.net/questions/11517/computer-algebra-errors

I don't know any interesting bugs in symbolic algebra packages but I know a true, enlightening and entertaining story about something that looked like a bug but wasn't.

Define sinc𝑥=(sin𝑥)/𝑥.

Someone found the following result in an algebra package: ∫∞0𝑑𝑥sinc𝑥=𝜋/2

They then found the following results:

...

So of course when they got:

∫∞0𝑑𝑥sinc𝑥sinc(𝑥/3)sinc(𝑥/5)⋯sinc(𝑥/15)=(467807924713440738696537864469/935615849440640907310521750000)𝜋

hmm:

Which means that nobody knows Fourier analysis nowdays. Very sad and discouraging story... – fedja Jan 29 '10 at 18:47

--

Because the most popular systems are all commercial, they tend to guard their bug database rather closely -- making them public would seriously cut their sales. For example, for the open source project Sage (which is quite young), you can get a list of all the known bugs from this page. 1582 known issues on Feb.16th 2010 (which includes feature requests, problems with documentation, etc).

That is an order of magnitude less than the commercial systems. And it's not because it is better, it is because it is younger and smaller. It might be better, but until SAGE does a lot of analysis (about 40% of CAS bugs are there) and a fancy user interface (another 40%), it is too hard to compare.

I once ran a graduate course whose core topic was studying the fundamental disconnect between the algebraic nature of CAS and the analytic nature of the what it is mostly used for. There are issues of logic -- CASes work more or less in an intensional logic, while most of analysis is stated in a purely extensional fashion. There is no well-defined 'denotational semantics' for expressions-as-functions, which strongly contributes to the deeper bugs in CASes.]

...

Should such widely-believed conjectures as P≠NP or the Riemann hypothesis turn out be false, then because they are assumed by so many existing proofs, a far larger math holocaust would ensue38 - and our previous estimates of error rates will turn out to have been substantial underestimates. But it may be a cloud with a silver lining, if it doesn’t come at a time of danger.

https://mathoverflow.net/questions/338607/why-doesnt-mathematics-collapse-down-even-though-humans-quite-often-make-mista

more on formal methods in programming:

https://www.quantamagazine.org/formal-verification-creates-hacker-proof-code-20160920/

https://intelligence.org/2014/03/02/bob-constable/

https://softwareengineering.stackexchange.com/questions/375342/what-are-the-barriers-that-prevent-widespread-adoption-of-formal-methods

Update: measured effort

In the October 2018 issue of Communications of the ACM there is an interesting article about Formally verified software in the real world with some estimates of the effort.

Interestingly (based on OS development for military equipment), it seems that producing formally proved software requires 3.3 times more effort than with traditional engineering techniques. So it's really costly.

On the other hand, it requires 2.3 times less effort to get high security software this way than with traditionally engineered software if you add the effort to make such software certified at a high security level (EAL 7). So if you have high reliability or security requirements there is definitively a business case for going formal.

WHY DON'T PEOPLE USE FORMAL METHODS?: https://www.hillelwayne.com/post/why-dont-people-use-formal-methods/

You can see examples of how all of these look at Let’s Prove Leftpad. HOL4 and Isabelle are good examples of “independent theorem” specs, SPARK and Dafny have “embedded assertion” specs, and Coq and Agda have “dependent type” specs.6

If you squint a bit it looks like these three forms of code spec map to the three main domains of automated correctness checking: tests, contracts, and types. This is not a coincidence. Correctness is a spectrum, and formal verification is one extreme of that spectrum. As we reduce the rigour (and effort) of our verification we get simpler and narrower checks, whether that means limiting the explored state space, using weaker types, or pushing verification to the runtime. Any means of total specification then becomes a means of partial specification, and vice versa: many consider Cleanroom a formal verification technique, which primarily works by pushing code review far beyond what’s humanly possible.

...

The question, then: “is 90/95/99% correct significantly cheaper than 100% correct?” The answer is very yes. We all are comfortable saying that a codebase we’ve well-tested and well-typed is mostly correct modulo a few fixes in prod, and we’re even writing more than four lines of code a day. In fact, the vast… [more]

ratty
gwern
analysis
essay
realness
truth
correctness
reason
philosophy
math
proofs
formal-methods
cs
programming
engineering
worse-is-better/the-right-thing
intuition
giants
old-anglo
error
street-fighting
heuristic
zooming
risk
threat-modeling
software
lens
logic
inference
physics
differential
geometry
estimate
distribution
robust
speculation
nonlinearity
cost-benefit
convexity-curvature
measure
scale
trivia
cocktail
history
early-modern
europe
math.CA
rigor
news
org:mag
org:sci
miri-cfar
pdf
thesis
comparison
examples
org:junk
q-n-a
stackex
pragmatic
tradeoffs
cracker-prog
techtariat
invariance
DSL
chart
ecosystem
grokkability
heavyweights
CAS
static-dynamic
lower-bounds
complexity
tcs
open-problems
big-surf
ideas
certificates-recognition
proof-systems
PCP
mediterranean
SDP
meta:prediction
epistemic
questions
guessing
distributed
overflow
nibble
soft-question
track-record
big-list
hmm
frontier
state-of-art
1. Mistakes where the theorem is still true, but the proof was incorrect (type I)

2. Mistakes where the theorem was false, and the proof was also necessarily incorrect (type II)

Before someone comes up with a final answer, a mathematician may have many levels of intuition in formulating & working on the problem, but we’ll consider the final end-product where the mathematician feels satisfied that he has solved it. Case 1 is perhaps the most common case, with innumerable examples; this is sometimes due to mistakes in the proof that anyone would accept is a mistake, but many of these cases are due to changing standards of proof. For example, when David Hilbert discovered errors in Euclid’s proofs which no one noticed before, the theorems were still true, and the gaps more due to Hilbert being a modern mathematician thinking in terms of formal systems (which of course Euclid did not think in). (David Hilbert himself turns out to be a useful example of the other kind of error: his famous list of 23 problems was accompanied by definite opinions on the outcome of each problem and sometimes timings, several of which were wrong or questionable5.) Similarly, early calculus used ‘infinitesimals’ which were sometimes treated as being 0 and sometimes treated as an indefinitely small non-zero number; this was incoherent and strictly speaking, practically all of the calculus results were wrong because they relied on an incoherent concept - but of course the results were some of the greatest mathematical work ever conducted6 and when later mathematicians put calculus on a more rigorous footing, they immediately re-derived those results (sometimes with important qualifications), and doubtless as modern math evolves other fields have sometimes needed to go back and clean up the foundations and will in the future.7

...

Isaac Newton, incidentally, gave two proofs of the same solution to a problem in probability, one via enumeration and the other more abstract; the enumeration was correct, but the other proof totally wrong and this was not noticed for a long time, leading Stigler to remark:

...

TYPE I > TYPE II?

“Lefschetz was a purely intuitive mathematician. It was said of him that he had never given a completely correct proof, but had never made a wrong guess either.”

- Gian-Carlo Rota13

Case 2 is disturbing, since it is a case in which we wind up with false beliefs and also false beliefs about our beliefs (we no longer know that we don’t know). Case 2 could lead to extinction.

...

Except, errors do not seem to be evenly & randomly distributed between case 1 and case 2. There seem to be far more case 1s than case 2s, as already mentioned in the early calculus example: far more than 50% of the early calculus results were correct when checked more rigorously. Richard Hamming attributes to Ralph Boas a comment that while editing Mathematical Reviews that “of the new results in the papers reviewed most are true but the corresponding proofs are perhaps half the time plain wrong”.

...

Gian-Carlo Rota gives us an example with Hilbert:

...

Olga labored for three years; it turned out that all mistakes could be corrected without any major changes in the statement of the theorems. There was one exception, a paper Hilbert wrote in his old age, which could not be fixed; it was a purported proof of the continuum hypothesis, you will find it in a volume of the Mathematische Annalen of the early thirties.

...

Leslie Lamport advocates for machine-checked proofs and a more rigorous style of proofs similar to natural deduction, noting a mathematician acquaintance guesses at a broad error rate of 1/329 and that he routinely found mistakes in his own proofs and, worse, believed false conjectures30.

[more on these "structured proofs":

https://academia.stackexchange.com/questions/52435/does-anyone-actually-publish-structured-proofs

https://mathoverflow.net/questions/35727/community-experiences-writing-lamports-structured-proofs

]

We can probably add software to that list: early software engineering work found that, dismayingly, bug rates seem to be simply a function of lines of code, and one would expect diseconomies of scale. So one would expect that in going from the ~4,000 lines of code of the Microsoft DOS operating system kernel to the ~50,000,000 lines of code in Windows Server 2003 (with full systems of applications and libraries being even larger: the comprehensive Debian repository in 2007 contained ~323,551,126 lines of code) that the number of active bugs at any time would be… fairly large. Mathematical software is hopefully better, but practitioners still run into issues (eg Durán et al 2014, Fonseca et al 2017) and I don’t know of any research pinning down how buggy key mathematical systems like Mathematica are or how much published mathematics may be erroneous due to bugs. This general problem led to predictions of doom and spurred much research into automated proof-checking, static analysis, and functional languages31.

[related:

https://mathoverflow.net/questions/11517/computer-algebra-errors

I don't know any interesting bugs in symbolic algebra packages but I know a true, enlightening and entertaining story about something that looked like a bug but wasn't.

Define sinc𝑥=(sin𝑥)/𝑥.

Someone found the following result in an algebra package: ∫∞0𝑑𝑥sinc𝑥=𝜋/2

They then found the following results:

...

So of course when they got:

∫∞0𝑑𝑥sinc𝑥sinc(𝑥/3)sinc(𝑥/5)⋯sinc(𝑥/15)=(467807924713440738696537864469/935615849440640907310521750000)𝜋

hmm:

Which means that nobody knows Fourier analysis nowdays. Very sad and discouraging story... – fedja Jan 29 '10 at 18:47

--

Because the most popular systems are all commercial, they tend to guard their bug database rather closely -- making them public would seriously cut their sales. For example, for the open source project Sage (which is quite young), you can get a list of all the known bugs from this page. 1582 known issues on Feb.16th 2010 (which includes feature requests, problems with documentation, etc).

That is an order of magnitude less than the commercial systems. And it's not because it is better, it is because it is younger and smaller. It might be better, but until SAGE does a lot of analysis (about 40% of CAS bugs are there) and a fancy user interface (another 40%), it is too hard to compare.

I once ran a graduate course whose core topic was studying the fundamental disconnect between the algebraic nature of CAS and the analytic nature of the what it is mostly used for. There are issues of logic -- CASes work more or less in an intensional logic, while most of analysis is stated in a purely extensional fashion. There is no well-defined 'denotational semantics' for expressions-as-functions, which strongly contributes to the deeper bugs in CASes.]

...

Should such widely-believed conjectures as P≠NP or the Riemann hypothesis turn out be false, then because they are assumed by so many existing proofs, a far larger math holocaust would ensue38 - and our previous estimates of error rates will turn out to have been substantial underestimates. But it may be a cloud with a silver lining, if it doesn’t come at a time of danger.

https://mathoverflow.net/questions/338607/why-doesnt-mathematics-collapse-down-even-though-humans-quite-often-make-mista

more on formal methods in programming:

https://www.quantamagazine.org/formal-verification-creates-hacker-proof-code-20160920/

https://intelligence.org/2014/03/02/bob-constable/

https://softwareengineering.stackexchange.com/questions/375342/what-are-the-barriers-that-prevent-widespread-adoption-of-formal-methods

Update: measured effort

In the October 2018 issue of Communications of the ACM there is an interesting article about Formally verified software in the real world with some estimates of the effort.

Interestingly (based on OS development for military equipment), it seems that producing formally proved software requires 3.3 times more effort than with traditional engineering techniques. So it's really costly.

On the other hand, it requires 2.3 times less effort to get high security software this way than with traditionally engineered software if you add the effort to make such software certified at a high security level (EAL 7). So if you have high reliability or security requirements there is definitively a business case for going formal.

WHY DON'T PEOPLE USE FORMAL METHODS?: https://www.hillelwayne.com/post/why-dont-people-use-formal-methods/

You can see examples of how all of these look at Let’s Prove Leftpad. HOL4 and Isabelle are good examples of “independent theorem” specs, SPARK and Dafny have “embedded assertion” specs, and Coq and Agda have “dependent type” specs.6

If you squint a bit it looks like these three forms of code spec map to the three main domains of automated correctness checking: tests, contracts, and types. This is not a coincidence. Correctness is a spectrum, and formal verification is one extreme of that spectrum. As we reduce the rigour (and effort) of our verification we get simpler and narrower checks, whether that means limiting the explored state space, using weaker types, or pushing verification to the runtime. Any means of total specification then becomes a means of partial specification, and vice versa: many consider Cleanroom a formal verification technique, which primarily works by pushing code review far beyond what’s humanly possible.

...

The question, then: “is 90/95/99% correct significantly cheaper than 100% correct?” The answer is very yes. We all are comfortable saying that a codebase we’ve well-tested and well-typed is mostly correct modulo a few fixes in prod, and we’re even writing more than four lines of code a day. In fact, the vast… [more]

10 weeks ago by nhaliday

Research Debt

techtariat acmtariat rhetoric contrarianism research debt academia communication writing science meta:science better-explained worrydream coordination bret-victor michael-nielsen tech links thurston overflow discussion org:bleg nibble 🔬 🖥 🎓 visual-understanding the-trenches impact meta:research metameta big-picture hi-order-bits info-dynamics elegance meta:reading technical-writing heavyweights

march 2017 by nhaliday

techtariat acmtariat rhetoric contrarianism research debt academia communication writing science meta:science better-explained worrydream coordination bret-victor michael-nielsen tech links thurston overflow discussion org:bleg nibble 🔬 🖥 🎓 visual-understanding the-trenches impact meta:research metameta big-picture hi-order-bits info-dynamics elegance meta:reading technical-writing heavyweights

march 2017 by nhaliday

Peter Norvig, the meaning of polynomials, debugging as psychotherapy | Quomodocumque

march 2017 by nhaliday

He briefly showed a demo where, given values of a polynomial, a machine can put together a few lines of code that successfully computes the polynomial. But the code looks weird to a human eye. To compute some quadratic, it nests for-loops and adds things up in a funny way that ends up giving the right output. So has it really ”learned” the polynomial? I think in computer science, you typically feel you’ve learned a function if you can accurately predict its value on a given input. For an algebraist like me, a function determines but isn’t determined by the values it takes; to me, there’s something about that quadratic polynomial the machine has failed to grasp. I don’t think there’s a right or wrong answer here, just a cultural difference to be aware of. Relevant: Norvig’s description of “the two cultures” at the end of this long post on natural language processing (which is interesting all the way through!)

mathtariat
org:bleg
nibble
tech
ai
talks
summary
philosophy
lens
comparison
math
cs
tcs
polynomials
nlp
debugging
psychology
cog-psych
complex-systems
deep-learning
analogy
legibility
interpretability
composition-decomposition
coupling-cohesion
apollonian-dionysian
heavyweights
march 2017 by nhaliday

An Introduction to Measure Theory - Terence Tao

books draft unit math gowers mathtariat measure math.CA probability yoga problem-solving pdf tricki local-global counterexample visual-understanding lifts-projections oscillation limits estimate quantifiers-sums synthesis coarse-fine p:someday s:** heavyweights

february 2017 by nhaliday

books draft unit math gowers mathtariat measure math.CA probability yoga problem-solving pdf tricki local-global counterexample visual-understanding lifts-projections oscillation limits estimate quantifiers-sums synthesis coarse-fine p:someday s:** heavyweights

february 2017 by nhaliday

Mikhail Leonidovich Gromov - Wikipedia

january 2017 by nhaliday

Gromov's style of geometry often features a "coarse" or "soft" viewpoint, analyzing asymptotic or large-scale properties.

Gromov is also interested in mathematical biology,[11] the structure of the brain and the thinking process, and the way scientific ideas evolve.[8]

math
people
russia
differential
geometry
topology
math.GR
wiki
structure
meta:math
meta:science
interdisciplinary
bio
neuro
magnitude
limits
science
nibble
coarse-fine
wild-ideas
convergence
info-dynamics
ideas
heavyweights
Gromov is also interested in mathematical biology,[11] the structure of the brain and the thinking process, and the way scientific ideas evolve.[8]

january 2017 by nhaliday

In Computers We Trust? | Quanta Magazine

january 2017 by nhaliday

As math grows ever more complex, will computers reign?

Shalosh B. Ekhad is a computer. Or, rather, it is any of a rotating cast of computers used by the mathematician Doron Zeilberger, from the Dell in his New Jersey office to a supercomputer whose services he occasionally enlists in Austria. The name — Hebrew for “three B one” — refers to the AT&T 3B1, Ekhad’s earliest incarnation.

“The soul is the software,” said Zeilberger, who writes his own code using a popular math programming tool called Maple.

news
org:mag
org:sci
popsci
math
culture
academia
automation
formal-methods
ai
debate
interdisciplinary
rigor
proofs
nibble
org:inst
calculation
bare-hands
heavyweights
contrarianism
computation
correctness
oss
replication
logic
frontier
state-of-art
Shalosh B. Ekhad is a computer. Or, rather, it is any of a rotating cast of computers used by the mathematician Doron Zeilberger, from the Dell in his New Jersey office to a supercomputer whose services he occasionally enlists in Austria. The name — Hebrew for “three B one” — refers to the AT&T 3B1, Ekhad’s earliest incarnation.

“The soul is the software,” said Zeilberger, who writes his own code using a popular math programming tool called Maple.

january 2017 by nhaliday

soft question - Thinking and Explaining - MathOverflow

january 2017 by nhaliday

- good question from Bill Thurston

- great answers by Terry Tao, fedja, Minhyong Kim, gowers, etc.

Terry Tao:

- symmetry as blurring/vibrating/wobbling, scale invariance

- anthropomorphization, adversarial perspective for estimates/inequalities/quantifiers, spending/economy

fedja walks through his though-process from another answer

Minhyong Kim: anthropology of mathematical philosophizing

Per Vognsen: normality as isotropy

comment: conjugate subgroup gHg^-1 ~ "H but somewhere else in G"

gowers: hidden things in basic mathematics/arithmetic

comment by Ryan Budney: x sin(x) via x -> (x, sin(x)), (x, y) -> xy

I kinda get what he's talking about but needed to use Mathematica to get the initial visualization down.

To remind myself later:

- xy can be easily visualized by juxtaposing the two parabolae x^2 and -x^2 diagonally

- x sin(x) can be visualized along that surface by moving your finger along the line (x, 0) but adding some oscillations in y direction according to sin(x)

q-n-a
soft-question
big-list
intuition
communication
teaching
math
thinking
writing
thurston
lens
overflow
synthesis
hi-order-bits
👳
insight
meta:math
clarity
nibble
giants
cartoons
gowers
mathtariat
better-explained
stories
the-trenches
problem-solving
homogeneity
symmetry
fedja
examples
philosophy
big-picture
vague
isotropy
reflection
spatial
ground-up
visual-understanding
polynomials
dimensionality
math.GR
worrydream
scholar
🎓
neurons
metabuch
yoga
retrofit
mental-math
metameta
wisdom
wordlessness
oscillation
operational
adversarial
quantifiers-sums
exposition
explanation
tricki
concrete
s:***
manifolds
invariance
dynamical
info-dynamics
cool
direction
elegance
heavyweights
analysis
guessing
- great answers by Terry Tao, fedja, Minhyong Kim, gowers, etc.

Terry Tao:

- symmetry as blurring/vibrating/wobbling, scale invariance

- anthropomorphization, adversarial perspective for estimates/inequalities/quantifiers, spending/economy

fedja walks through his though-process from another answer

Minhyong Kim: anthropology of mathematical philosophizing

Per Vognsen: normality as isotropy

comment: conjugate subgroup gHg^-1 ~ "H but somewhere else in G"

gowers: hidden things in basic mathematics/arithmetic

comment by Ryan Budney: x sin(x) via x -> (x, sin(x)), (x, y) -> xy

I kinda get what he's talking about but needed to use Mathematica to get the initial visualization down.

To remind myself later:

- xy can be easily visualized by juxtaposing the two parabolae x^2 and -x^2 diagonally

- x sin(x) can be visualized along that surface by moving your finger along the line (x, 0) but adding some oscillations in y direction according to sin(x)

january 2017 by nhaliday

On “local” and “global” errors in mathematical papers, and how to detect them

november 2016 by nhaliday

local vs. global errors in technical papers

old:

https://plus.google.com/+TerenceTao27/posts/78aoEHoPhpS

gowers
social
metabuch
thinking
problem-solving
math
advice
reflection
scholar
🎓
expert
mathtariat
lens
local-global
meta:math
cartoons
learning
the-trenches
meta:research
s:**
info-dynamics
studying
expert-experience
meta:reading
multi
heavyweights
old:

https://plus.google.com/+TerenceTao27/posts/78aoEHoPhpS

november 2016 by nhaliday

On “compilation errors” in mathematical reading, and how to resolve them

november 2016 by nhaliday

compilation errors in academic papers

old:

[Google Buzz closed down for good recently, so I will be reprinting a small n...

https://plus.google.com/u/0/+TerenceTao27/posts/TGjjJPUdJjk

gowers
social
advice
reflection
math
thinking
problem-solving
metabuch
expert
scholar
🎓
mathtariat
lens
meta:math
cartoons
learning
lifts-projections
the-trenches
meta:research
s:**
info-dynamics
studying
expert-experience
meta:reading
analogy
compilers
multi
heavyweights
zooming
old:

[Google Buzz closed down for good recently, so I will be reprinting a small n...

https://plus.google.com/u/0/+TerenceTao27/posts/TGjjJPUdJjk

november 2016 by nhaliday

The capacity to be alone | Quomodocumque

september 2016 by nhaliday

In fact, most of these comrades who I gauged to be more brilliant than I have gone on to become distinguished mathematicians. Still from the perspective or thirty or thirty five years, I can state that their imprint upon the mathematics of our time has not been very profound. They’ve done all things, often beautiful things in a context that was already set out before them, which they had no inclination to disturb. Without being aware of it, they’ve remained prisoners of those invisible and despotic circles which delimit the universe of a certain milieu in a given era. To have broken these bounds they would have to rediscover in themselves that capability which was their birthright, as it was mine: The capacity to be alone.

math
reflection
quotes
scholar
mathtariat
lens
optimate
serene
individualism-collectivism
the-monster
humility
the-trenches
virtu
courage
emotion
extra-introversion
allodium
ascetic
heavyweights
psychiatry
september 2016 by nhaliday

On proof and progress in mathematics

pdf thurston math writing thinking synthesis papers essay unit nibble intuition worrydream communication proofs the-trenches reflection geometry meta:math better-explained stories virtu 🎓 scholar metameta wisdom narrative p:whenever inference cs programming rigor formal-methods meta:research info-dynamics elegance technical-writing heavyweights guessing

august 2016 by nhaliday

pdf thurston math writing thinking synthesis papers essay unit nibble intuition worrydream communication proofs the-trenches reflection geometry meta:math better-explained stories virtu 🎓 scholar metameta wisdom narrative p:whenever inference cs programming rigor formal-methods meta:research info-dynamics elegance technical-writing heavyweights guessing

august 2016 by nhaliday

ho.history overview - Does any research mathematics involve solving functional equations? - MathOverflow

math reflection expert characterization tidbits q-n-a overflow oly mathtariat gowers motivation nibble expert-experience rec-math heavyweights explanation roots explanans properties

july 2016 by nhaliday

math reflection expert characterization tidbits q-n-a overflow oly mathtariat gowers motivation nibble expert-experience rec-math heavyweights explanation roots explanans properties

july 2016 by nhaliday

notation - Why does mathematical convention deal so ineptly with multisets? - Mathematics Stack Exchange

thinking language math history q-n-a worrydream thurston overflow soft-question notation meta:math intricacy conceptual-vocab nibble elegance worse-is-better/the-right-thing heavyweights

july 2016 by nhaliday

thinking language math history q-n-a worrydream thurston overflow soft-question notation meta:math intricacy conceptual-vocab nibble elegance worse-is-better/the-right-thing heavyweights

july 2016 by nhaliday

soft question - Famous mathematical quotes - MathOverflow

math aphorism reflection list quotes q-n-a overflow soft-question big-list mathtariat stories lens nibble giants von-neumann darwinian old-anglo poetry letters troll lol creative algebra geometry linear-algebra thick-thin moments high-variance elegance heavyweights

june 2016 by nhaliday

math aphorism reflection list quotes q-n-a overflow soft-question big-list mathtariat stories lens nibble giants von-neumann darwinian old-anglo poetry letters troll lol creative algebra geometry linear-algebra thick-thin moments high-variance elegance heavyweights

june 2016 by nhaliday

soft question - How do you not forget old math? - MathOverflow

june 2016 by nhaliday

Terry Tao:

I find that blogging about material that I would otherwise forget eventually is extremely valuable in this regard. (I end up consulting my own blog posts on a regular basis.) EDIT: and now I remember I already wrote on this topic: terrytao.wordpress.com/career-advice/write-down-what-youve-done

fedja:

The only way to cope with this loss of memory I know is to do some reading on systematic basis. Of course, if you read one paper in algebraic geometry (or whatever else) a month (or even two months), you may not remember the exact content of all of them by the end of the year but, since all mathematicians in one field use pretty much the same tricks and draw from pretty much the same general knowledge, you'll keep the core things in your memory no matter what you read (provided it is not patented junk, of course) and this is about as much as you can hope for.

Relating abstract things to "real life stuff" (and vice versa) is automatic when you work as a mathematician. For me, the proof of the Chacon-Ornstein ergodic theorem is just a sandpile moving over a pit with the sand falling down after every shift. I often tell my students that every individual term in the sequence doesn't matter at all for the limit but somehow together they determine it like no individual human is of any real importance while together they keep this civilization running, etc. No special effort is needed here and, moreover, if the analogy is not natural but contrived, it'll not be helpful or memorable. The standard mnemonic techniques are pretty useless in math. IMHO (the famous "foil" rule for the multiplication of sums of two terms is inferior to the natural "pair each term in the first sum with each term in the second sum" and to the picture of a rectangle tiled with smaller rectangles, though, of course, the foil rule sounds way more sexy).

One thing that I don't think the other respondents have emphasized enough is that you should work on prioritizing what you choose to study and remember.

Timothy Chow:

As others have said, forgetting lots of stuff is inevitable. But there are ways you can mitigate the damage of this information loss. I find that a useful technique is to try to organize your knowledge hierarchically. Start by coming up with a big picture, and make sure you understand and remember that picture thoroughly. Then drill down to the next level of detail, and work on remembering that. For example, if I were trying to remember everything in a particular book, I might start by memorizing the table of contents, and then I'd work on remembering the theorem statements, and then finally the proofs. (Don't take this illustration too literally; it's better to come up with your own conceptual hierarchy than to slavishly follow the formal hierarchy of a published text. But I do think that a hierarchical approach is valuable.)

Organizing your knowledge like this helps you prioritize. You can then consciously decide that certain large swaths of knowledge are not worth your time at the moment, and just keep a "stub" in memory to remind you that that body of knowledge exists, should you ever need to dive into it. In areas of higher priority, you can plunge more deeply. By making sure you thoroughly internalize the top levels of the hierarchy, you reduce the risk of losing sight of entire areas of important knowledge. Generally it's less catastrophic to forget the details than to forget about a whole region of the big picture, because you can often revisit the details as long as you know what details you need to dig up. (This is fortunate since the details are the most memory-intensive.)

Having a hierarchy also helps you accrue new knowledge. Often when you encounter something new, you can relate it to something you already know, and file it in the same branch of your mental tree.

thinking
math
growth
advice
expert
q-n-a
🎓
long-term
tradeoffs
scholar
overflow
soft-question
gowers
mathtariat
ground-up
hi-order-bits
intuition
synthesis
visual-understanding
decision-making
scholar-pack
cartoons
lens
big-picture
ergodic
nibble
zooming
trees
fedja
reflection
retention
meta:research
wisdom
skeleton
practice
prioritizing
concrete
s:***
info-dynamics
knowledge
studying
the-trenches
chart
expert-experience
quixotic
elegance
heavyweights
I find that blogging about material that I would otherwise forget eventually is extremely valuable in this regard. (I end up consulting my own blog posts on a regular basis.) EDIT: and now I remember I already wrote on this topic: terrytao.wordpress.com/career-advice/write-down-what-youve-done

fedja:

The only way to cope with this loss of memory I know is to do some reading on systematic basis. Of course, if you read one paper in algebraic geometry (or whatever else) a month (or even two months), you may not remember the exact content of all of them by the end of the year but, since all mathematicians in one field use pretty much the same tricks and draw from pretty much the same general knowledge, you'll keep the core things in your memory no matter what you read (provided it is not patented junk, of course) and this is about as much as you can hope for.

Relating abstract things to "real life stuff" (and vice versa) is automatic when you work as a mathematician. For me, the proof of the Chacon-Ornstein ergodic theorem is just a sandpile moving over a pit with the sand falling down after every shift. I often tell my students that every individual term in the sequence doesn't matter at all for the limit but somehow together they determine it like no individual human is of any real importance while together they keep this civilization running, etc. No special effort is needed here and, moreover, if the analogy is not natural but contrived, it'll not be helpful or memorable. The standard mnemonic techniques are pretty useless in math. IMHO (the famous "foil" rule for the multiplication of sums of two terms is inferior to the natural "pair each term in the first sum with each term in the second sum" and to the picture of a rectangle tiled with smaller rectangles, though, of course, the foil rule sounds way more sexy).

One thing that I don't think the other respondents have emphasized enough is that you should work on prioritizing what you choose to study and remember.

Timothy Chow:

As others have said, forgetting lots of stuff is inevitable. But there are ways you can mitigate the damage of this information loss. I find that a useful technique is to try to organize your knowledge hierarchically. Start by coming up with a big picture, and make sure you understand and remember that picture thoroughly. Then drill down to the next level of detail, and work on remembering that. For example, if I were trying to remember everything in a particular book, I might start by memorizing the table of contents, and then I'd work on remembering the theorem statements, and then finally the proofs. (Don't take this illustration too literally; it's better to come up with your own conceptual hierarchy than to slavishly follow the formal hierarchy of a published text. But I do think that a hierarchical approach is valuable.)

Organizing your knowledge like this helps you prioritize. You can then consciously decide that certain large swaths of knowledge are not worth your time at the moment, and just keep a "stub" in memory to remind you that that body of knowledge exists, should you ever need to dive into it. In areas of higher priority, you can plunge more deeply. By making sure you thoroughly internalize the top levels of the hierarchy, you reduce the risk of losing sight of entire areas of important knowledge. Generally it's less catastrophic to forget the details than to forget about a whole region of the big picture, because you can often revisit the details as long as you know what details you need to dig up. (This is fortunate since the details are the most memory-intensive.)

Having a hierarchy also helps you accrue new knowledge. Often when you encounter something new, you can relate it to something you already know, and file it in the same branch of your mental tree.

june 2016 by nhaliday

Answer to What is it like to understand advanced mathematics? - Quora

may 2016 by nhaliday

thinking like a mathematician

some of the points:

- small # of tricks (echoes Rota)

- web of concepts and modularization (zooming out) allow quick reasoning

- comfort w/ ambiguity and lack of understanding, study high-dimensional objects via projections

- above is essential for research (and often what distinguishes research mathematicians from people who were good at math, or majored in math)

math
reflection
thinking
intuition
expert
synthesis
wormholes
insight
q-n-a
🎓
metabuch
tricks
scholar
problem-solving
aphorism
instinct
heuristic
lens
qra
soft-question
curiosity
meta:math
ground-up
cartoons
analytical-holistic
lifts-projections
hi-order-bits
scholar-pack
nibble
the-trenches
innovation
novelty
zooming
tricki
virtu
humility
metameta
wisdom
abstraction
skeleton
s:***
knowledge
expert-experience
elegance
judgement
advanced
heavyweights
guessing
some of the points:

- small # of tricks (echoes Rota)

- web of concepts and modularization (zooming out) allow quick reasoning

- comfort w/ ambiguity and lack of understanding, study high-dimensional objects via projections

- above is essential for research (and often what distinguishes research mathematicians from people who were good at math, or majored in math)

may 2016 by nhaliday

Reflections on the recent solution of the cap-set problem I | Gowers's Weblog

may 2016 by nhaliday

As regular readers of this blog will know, I have a strong interest in the question of where mathematical ideas come from, and a strong conviction that they always result from a fairly systematic process — and that the opposite impression, that some ideas are incredible bolts from the blue that require “genius” or “sudden inspiration” to find, is an illusion that results from the way mathematicians present their proofs after they have discovered them.

math
research
academia
gowers
hmm
mathtariat
org:bleg
nibble
big-surf
algebraic-complexity
math.CO
questions
heavyweights
exposition
technical-writing
roots
problem-solving
polynomials
linear-algebra
motivation
guessing
may 2016 by nhaliday

The man who knew partition asymptotics | Annoying Precision

may 2016 by nhaliday

nice coverage of saddle point method

yoga
acm
math.CA
math
exposition
tidbits
mathtariat
oly
limits
math.CO
alg-combo
film
giants
org:bleg
nibble
stirling
clever-rats
AMT
heavyweights
may 2016 by nhaliday

The Mathematician Ken Ono’s Life Inspired By Ramanujan | Quanta Magazine

may 2016 by nhaliday

This intellectual crucible produced the desired results — Ono studied mathematics and launched a promising academic career — but at great emotional cost. As a teenager, Ono became so desperate to escape his parents’ expectations that he dropped out of high school. He later earned admission to the University of Chicago but had an apathetic attitude toward his studies, preferring to party with his fraternity brothers. He eventually discovered a genuine enthusiasm for mathematics, became a professor, and started a family, but fear of failure still weighed so heavily on Ono that he attempted suicide while attending an academic conference. Only after he joined the Institute for Advanced Study himself did Ono begin to make peace with his upbringing.

profile
math
people
career
popsci
hmm
news
org:mag
org:sci
giants
math.NT
nibble
org:inst
heavyweights
may 2016 by nhaliday

Polymath 10 Emergency Post 5: The Erdos-Szemeredi Sunflower Conjecture is Now Proven. | Combinatorics and more

math gowers announcement algebraic-complexity tcs math.CO tcstariat mathtariat research org:mat polynomials additive-combo org:bleg nibble big-surf questions heavyweights

may 2016 by nhaliday

math gowers announcement algebraic-complexity tcs math.CO tcstariat mathtariat research org:mat polynomials additive-combo org:bleg nibble big-surf questions heavyweights

may 2016 by nhaliday

Making invisible understanding visible

may 2016 by nhaliday

I like the example of cyclic subgroups

visualization
worrydream
thinking
math
yoga
thurston
intuition
algebra
insight
👳
wormholes
visual-understanding
michael-nielsen
water
exocortex
2016
fourier
cartoons
tcstariat
techtariat
clarity
vague
org:bleg
nibble
better-explained
math.GR
bounded-cognition
metameta
wordlessness
meta:math
s:***
composition-decomposition
dynamical
info-dynamics
let-me-see
elegance
heavyweights
guessing
may 2016 by nhaliday

On writing | What's new

april 2016 by nhaliday

also: on reading papers

writing
papers
academia
math
tcs
advice
reflection
thinking
expert
gowers
long-term
🎓
checklists
grad-school
scholar
mathtariat
learning
nibble
org:bleg
meta:research
info-foraging
studying
p:whenever
s:*
info-dynamics
expert-experience
meta:reading
technical-writing
heavyweights
april 2016 by nhaliday

Work hard | What's new

april 2016 by nhaliday

Similarly, to be a “professional” mathematician, you need to not only work on your research problem(s), but you should also constantly be working on learning new proofs and techniques, going over important proofs and papers time and again until you’ve mastered them. Don’t stay in your mathematical comfort zone, but expand your horizon by also reading (relevant) papers that are not at the heart of your own field. You should go to seminars to stay current and to challenge yourself to understand math in real time. And so on. All of these elements have to find their way into your daily work routine, because if you neglect any of them it will ultimately affect your research output negatively.

- from the comments

advice
academia
math
reflection
career
expert
gowers
long-term
🎓
aphorism
grad-school
phd
scholar
mathtariat
discipline
curiosity
🦉
nibble
org:bleg
the-trenches
meta:research
gtd
stamina
vitality
s:**
info-dynamics
expert-experience
heavyweights
- from the comments

april 2016 by nhaliday

Lean

january 2016 by nhaliday

https://lean-forward.github.io

The goal of the Lean Forward project is to collaborate with number theorists to formally prove theorems about research mathematics and to address the main usability issues hampering the adoption of proof assistants in mathematical circles. The theorems will be selected together with our collaborators to guide the development of formal libraries and verified tools.

mostly happening in the Netherlands

https://formalabstracts.github.io

A Review of the Lean Theorem Prover: https://jiggerwit.wordpress.com/2018/09/18/a-review-of-the-lean-theorem-prover/

- Thomas Hales

seems like a Coq might be a better starter if I ever try to get into proof assistants/theorem provers

An Argument for Controlled Natural Languages in Mathematics: https://jiggerwit.wordpress.com/2019/06/20/an-argument-for-controlled-natural-languages-in-mathematics/

By controlled natural language for mathematics (CNL), we mean an artificial language for the communication of mathematics that is (1) designed in a deliberate and explicit way with precise computer-readable syntax and semantics, (2) based on a single natural language (such as Chinese, Spanish, or English), and (3) broadly understood at least in an intuitive way by mathematically literate speakers of the natural language.

The definition of controlled natural language is intended to exclude invented languages such as Esperanto and Logjam that are not based on a single natural language. Programming languages are meant to be excluded, but a case might be made for TeX as the first broadly adopted controlled natural language for mathematics.

Perhaps it is best to start with an example. Here is a beautifully crafted CNL text created by Peter Koepke and Steffen Frerix. It reproduces a theorem and proof in Rudin’s Principles of mathematical analysis almost word for word. Their automated proof system is able to read and verify the proof.

https://github.com/Naproche/Naproche-SAD

research
math
formal-methods
msr
multi
homepage
research-program
skunkworks
math.NT
academia
ux
CAS
mathtariat
expert-experience
cost-benefit
nitty-gritty
review
critique
rant
types
learning
intricacy
functional
performance
c(pp)
ocaml-sml
comparison
ecosystem
DSL
tradeoffs
composition-decomposition
interdisciplinary
europe
germanic
grokkability
nlp
language
heavyweights
inference
rigor
automata-languages
repo
software
tools
syntax
frontier
state-of-art
pls
The goal of the Lean Forward project is to collaborate with number theorists to formally prove theorems about research mathematics and to address the main usability issues hampering the adoption of proof assistants in mathematical circles. The theorems will be selected together with our collaborators to guide the development of formal libraries and verified tools.

mostly happening in the Netherlands

https://formalabstracts.github.io

A Review of the Lean Theorem Prover: https://jiggerwit.wordpress.com/2018/09/18/a-review-of-the-lean-theorem-prover/

- Thomas Hales

seems like a Coq might be a better starter if I ever try to get into proof assistants/theorem provers

An Argument for Controlled Natural Languages in Mathematics: https://jiggerwit.wordpress.com/2019/06/20/an-argument-for-controlled-natural-languages-in-mathematics/

By controlled natural language for mathematics (CNL), we mean an artificial language for the communication of mathematics that is (1) designed in a deliberate and explicit way with precise computer-readable syntax and semantics, (2) based on a single natural language (such as Chinese, Spanish, or English), and (3) broadly understood at least in an intuitive way by mathematically literate speakers of the natural language.

The definition of controlled natural language is intended to exclude invented languages such as Esperanto and Logjam that are not based on a single natural language. Programming languages are meant to be excluded, but a case might be made for TeX as the first broadly adopted controlled natural language for mathematics.

Perhaps it is best to start with an example. Here is a beautifully crafted CNL text created by Peter Koepke and Steffen Frerix. It reproduces a theorem and proof in Rudin’s Principles of mathematical analysis almost word for word. Their automated proof system is able to read and verify the proof.

https://github.com/Naproche/Naproche-SAD

january 2016 by nhaliday

**related tags**

Copy this bookmark: