The Future of Mathematics? [video] | Hacker News

october 2019 by nhaliday

https://news.ycombinator.com/item?id=20909404

Kevin Buzzard (the Lean guy)

- general reflection on proof asssistants/theorem provers

- Kevin Hale's formal abstracts project, etc

- thinks of available theorem provers, Lean is "[the only one currently available that may be capable of formalizing all of mathematics eventually]" (goes into more detail right at the end, eg, quotient types)

hn
commentary
discussion
video
talks
presentation
math
formal-methods
expert-experience
msr
frontier
state-of-art
proofs
rigor
education
higher-ed
optimism
prediction
lens
search
meta:research
speculation
exocortex
skunkworks
automation
research
math.NT
big-surf
software
parsimony
cost-benefit
intricacy
correctness
programming
pls
python
functional
haskell
heavyweights
research-program
review
reflection
multi
pdf
slides
oly
experiment
span-cover
git
vcs
teaching
impetus
academia
composition-decomposition
coupling-cohesion
database
trust
types
plt
lifts-projections
induction
critique
beauty
truth
elegance
aesthetics
Kevin Buzzard (the Lean guy)

- general reflection on proof asssistants/theorem provers

- Kevin Hale's formal abstracts project, etc

- thinks of available theorem provers, Lean is "[the only one currently available that may be capable of formalizing all of mathematics eventually]" (goes into more detail right at the end, eg, quotient types)

october 2019 by nhaliday

The Existential Risk of Math Errors - Gwern.net

july 2019 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
move-fast-(and-break-things)
grokkability-clarity
technical-writing
trust
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]

july 2019 by nhaliday

Computer Scientists Close In on Unique Games Conjecture Proof | Quanta Magazine

news org:mag org:sci popsci tcs cs computation UGC complexity approximation lower-bounds hardness nibble org:inst rand-approx proofs big-surf announcement SDP optimization open-problems questions research

june 2018 by nhaliday

news org:mag org:sci popsci tcs cs computation UGC complexity approximation lower-bounds hardness nibble org:inst rand-approx proofs big-surf announcement SDP optimization open-problems questions research

june 2018 by nhaliday

[0712.3329] Universal Intelligence: A Definition of Machine Intelligence

april 2018 by nhaliday

- Shane Legg, Marcus Hutter

nibble
papers
org:mat
preprint
machine-learning
ai
intelligence
intricacy
definition
philosophy
psychology
cog-psych
psychometrics
decision-theory
order-disorder
deepgoog
flux-stasis
learning
list
links
quotes
rigor
lens
skeleton
metameta
search
problem-solving
generalization
complex-systems
cybernetics
volo-avolo
impetus
optimization
abstraction
big-peeps
academia
bio
measurement
universalism-particularism
big-picture
ideas
big-surf
synthesis
structure
large-factor
dimensionality
things
properties
detail-architecture
telos-atelos
values
descriptive
flexibility
occam
parsimony
cs
computation
bits
information-theory
complexity
absolute-relative
humanity
pragmatic
biases
turing
thick-thin
dennett
within-without
creative
theory-of-mind
nitty-gritty
spock
survey
reinforcement
april 2018 by nhaliday

[0706.3639] A Collection of Definitions of Intelligence

april 2018 by nhaliday

- Shane Legg, Marcus Hutter

nibble
papers
org:mat
preprint
machine-learning
ai
intelligence
intricacy
definition
philosophy
psychology
cog-psych
psychometrics
decision-theory
order-disorder
deepgoog
flux-stasis
learning
list
links
quotes
rigor
lens
skeleton
metameta
search
problem-solving
generalization
complex-systems
cybernetics
volo-avolo
impetus
optimization
abstraction
big-peeps
academia
bio
measurement
universalism-particularism
big-picture
ideas
big-surf
synthesis
things
properties
detail-architecture
telos-atelos
values
descriptive
flexibility
humanity
nitty-gritty
spock
survey
the-self
april 2018 by nhaliday

Information Processing: Mathematical Theory of Deep Neural Networks (Princeton workshop)

january 2018 by nhaliday

"Recently, long-past-due theoretical results have begun to emerge. These results, and those that will follow in their wake, will begin to shed light on the properties of large, adaptive, distributed learning architectures, and stand to revolutionize how computer science and neuroscience understand these systems."

hsu
scitariat
commentary
links
research
research-program
workshop
events
princeton
sanjeev-arora
deep-learning
machine-learning
ai
generalization
explanans
off-convex
nibble
frontier
speedometer
state-of-art
big-surf
announcement
january 2018 by nhaliday

New Theory Cracks Open the Black Box of Deep Learning | Quanta Magazine

september 2017 by nhaliday

A new idea called the “information bottleneck” is helping to explain the puzzling success of today’s artificial-intelligence algorithms — and might also explain how human brains learn.

sounds like he's just talking about autoencoders?

news
org:mag
org:sci
popsci
announcement
research
deep-learning
machine-learning
acm
information-theory
bits
neuro
model-class
big-surf
frontier
nibble
hmm
signal-noise
deepgoog
expert
ideas
wild-ideas
summary
talks
video
israel
roots
physics
interdisciplinary
ai
intelligence
shannon
giants
arrows
preimage
lifts-projections
composition-decomposition
characterization
markov
gradient-descent
papers
liner-notes
experiment
hi-order-bits
generalization
expert-experience
explanans
org:inst
speedometer
sounds like he's just talking about autoencoders?

september 2017 by nhaliday

Correlated Equilibria in Game Theory | Azimuth

july 2017 by nhaliday

Given this, it’s not surprising that Nash equilibria can be hard to find. Last September a paper came out making this precise, in a strong way:

• Yakov Babichenko and Aviad Rubinstein, Communication complexity of approximate Nash equilibria.

The authors show there’s no guaranteed method for players to find even an approximate Nash equilibrium unless they tell each other almost everything about their preferences. This makes finding the Nash equilibrium prohibitively difficult to find when there are lots of players… in general. There are particular games where it’s not difficult, and that makes these games important: for example, if you’re trying to run a government well. (A laughable notion these days, but still one can hope.)

Klarreich’s article in Quanta gives a nice readable account of this work and also a more practical alternative to the concept of Nash equilibrium. It’s called a ‘correlated equilibrium’, and it was invented by the mathematician Robert Aumann in 1974. You can see an attempt to define it here:

baez
org:bleg
nibble
mathtariat
commentary
summary
news
org:mag
org:sci
popsci
equilibrium
GT-101
game-theory
acm
conceptual-vocab
concept
definition
thinking
signaling
coordination
tcs
complexity
communication-complexity
lower-bounds
no-go
liner-notes
big-surf
papers
research
algorithmic-econ
volo-avolo
• Yakov Babichenko and Aviad Rubinstein, Communication complexity of approximate Nash equilibria.

The authors show there’s no guaranteed method for players to find even an approximate Nash equilibrium unless they tell each other almost everything about their preferences. This makes finding the Nash equilibrium prohibitively difficult to find when there are lots of players… in general. There are particular games where it’s not difficult, and that makes these games important: for example, if you’re trying to run a government well. (A laughable notion these days, but still one can hope.)

Klarreich’s article in Quanta gives a nice readable account of this work and also a more practical alternative to the concept of Nash equilibrium. It’s called a ‘correlated equilibrium’, and it was invented by the mathematician Robert Aumann in 1974. You can see an attempt to define it here:

july 2017 by nhaliday

Alzheimers | West Hunter

july 2017 by nhaliday

Some disease syndromes almost have to be caused by pathogens – for example, any with a fitness impact (prevalence x fitness reduction) > 2% or so, too big to be caused by mutational pressure. I don’t think that this is the case for AD: it hits so late in life that the fitness impact is minimal. However, that hardly means that it can’t be caused by a pathogen or pathogens – a big fraction of all disease syndromes are, including many that strike in old age. That possibility is always worth checking out, not least because infectious diseases are generally easier to prevent and/or treat.

There is new work that strongly suggests that pathogens are the root cause. It appears that the amyloid is an antimicrobial peptide. amyloid-beta binds to invading microbes and then surrounds and entraps them. ‘When researchers injected Salmonella into mice’s hippocampi, a brain area damaged in Alzheimer’s, A-beta quickly sprang into action. It swarmed the bugs and formed aggregates called fibrils and plaques. “Overnight you see the plaques throughout the hippocampus where the bugs were, and then in each single plaque is a single bacterium,” Tanzi says. ‘

obesity and pathogens: https://westhunt.wordpress.com/2016/05/29/alzheimers/#comment-79757

not sure about this guy, but interesting: https://westhunt.wordpress.com/2016/05/29/alzheimers/#comment-79748

http://perfecthealthdiet.com/2010/06/is-alzheimer%E2%80%99s-caused-by-a-bacterial-infection-of-the-brain/

https://westhunt.wordpress.com/2016/12/13/the-twelfth-battle-of-the-isonzo/

All too often we see large, long-lasting research efforts that never produce, never achieve their goal.

For example, the amyloid hypothesis [accumulation of amyloid-beta oligomers is the cause of Alzheimers] has been dominant for more than 20 years, and has driven development of something like 15 drugs. None of them have worked. At the same time the well-known increased risk from APOe4 has been almost entirely ignored, even though it ought to be a clue to the cause.

In general, when a research effort has been spinning its wheels for a generation or more, shouldn’t we try something different? We could at least try putting a fraction of those research dollars into alternative approaches that have not yet failed repeatedly.

Mostly this applies to research efforts that at least wish they were science. ‘educational research’ is in a special class, and I hardly know what to recommend. Most of the remedial actions that occur to me violate one or more of the Geneva conventions.

APOe4 related to lymphatic system: https://en.wikipedia.org/wiki/Apolipoprotein_E

https://westhunt.wordpress.com/2012/03/06/spontaneous-generation/#comment-2236

Look,if I could find out the sort of places that I usually misplace my keys – if I did, which I don’t – I could find the keys more easily the next time I lose them. If you find out that practitioners of a given field are not very competent, it marks that field as a likely place to look for relatively easy discovery. Thus medicine is a promising field, because on the whole doctors are not terribly good investigators. For example, none of the drugs developed for Alzheimers have worked at all, which suggests that our ideas on the causation of Alzheimers are likely wrong. Which suggests that it may (repeat may) be possible to make good progress on Alzheimers, either by an entirely empirical approach, which is way underrated nowadays, or by dumping the current explanation, finding a better one, and applying it.

You could start by looking at basic notions of field X and asking yourself: How do we really know that? Is there serious statistical evidence? Does that notion even accord with basic theory? This sort of checking is entirely possible. In most of the social sciences, we don’t, there isn’t, and it doesn’t.

Hygiene and the world distribution of Alzheimer’s disease: Epidemiological evidence for a relationship between microbial environment and age-adjusted disease burden: https://academic.oup.com/emph/article/2013/1/173/1861845/Hygiene-and-the-world-distribution-of-Alzheimer-s

Amyloid-β peptide protects against microbial infection in mouse and worm models of Alzheimer’s disease: http://stm.sciencemag.org/content/8/340/340ra72

Fungus, the bogeyman: http://www.economist.com/news/science-and-technology/21676754-curious-result-hints-possibility-dementia-caused-fungal

Fungus and dementia

paper: http://www.nature.com/articles/srep15015

Porphyromonas gingivalis in Alzheimer’s disease brains: Evidence for disease causation and treatment with small-molecule inhibitors: https://advances.sciencemag.org/content/5/1/eaau3333

west-hunter
scitariat
disease
parasites-microbiome
medicine
dementia
neuro
speculation
ideas
low-hanging
todo
immune
roots
the-bones
big-surf
red-queen
multi
🌞
poast
obesity
strategy
info-foraging
info-dynamics
institutions
meta:medicine
social-science
curiosity
🔬
science
meta:science
meta:research
wiki
epidemiology
public-health
study
arbitrage
alt-inst
correlation
cliometrics
path-dependence
street-fighting
methodology
nibble
population-genetics
org:nat
health
embodied
longevity
aging
org:rec
org:biz
org:anglo
news
neuro-nitgrit
candidate-gene
nutrition
diet
org:health
explanans
fashun
empirical
theory-practice
ability-competence
dirty-hands
education
aphorism
truth
westminster
innovation
evidence-based
religion
prudence
track-record
problem-solving
dental
being-right
prioritizing
There is new work that strongly suggests that pathogens are the root cause. It appears that the amyloid is an antimicrobial peptide. amyloid-beta binds to invading microbes and then surrounds and entraps them. ‘When researchers injected Salmonella into mice’s hippocampi, a brain area damaged in Alzheimer’s, A-beta quickly sprang into action. It swarmed the bugs and formed aggregates called fibrils and plaques. “Overnight you see the plaques throughout the hippocampus where the bugs were, and then in each single plaque is a single bacterium,” Tanzi says. ‘

obesity and pathogens: https://westhunt.wordpress.com/2016/05/29/alzheimers/#comment-79757

not sure about this guy, but interesting: https://westhunt.wordpress.com/2016/05/29/alzheimers/#comment-79748

http://perfecthealthdiet.com/2010/06/is-alzheimer%E2%80%99s-caused-by-a-bacterial-infection-of-the-brain/

https://westhunt.wordpress.com/2016/12/13/the-twelfth-battle-of-the-isonzo/

All too often we see large, long-lasting research efforts that never produce, never achieve their goal.

For example, the amyloid hypothesis [accumulation of amyloid-beta oligomers is the cause of Alzheimers] has been dominant for more than 20 years, and has driven development of something like 15 drugs. None of them have worked. At the same time the well-known increased risk from APOe4 has been almost entirely ignored, even though it ought to be a clue to the cause.

In general, when a research effort has been spinning its wheels for a generation or more, shouldn’t we try something different? We could at least try putting a fraction of those research dollars into alternative approaches that have not yet failed repeatedly.

Mostly this applies to research efforts that at least wish they were science. ‘educational research’ is in a special class, and I hardly know what to recommend. Most of the remedial actions that occur to me violate one or more of the Geneva conventions.

APOe4 related to lymphatic system: https://en.wikipedia.org/wiki/Apolipoprotein_E

https://westhunt.wordpress.com/2012/03/06/spontaneous-generation/#comment-2236

Look,if I could find out the sort of places that I usually misplace my keys – if I did, which I don’t – I could find the keys more easily the next time I lose them. If you find out that practitioners of a given field are not very competent, it marks that field as a likely place to look for relatively easy discovery. Thus medicine is a promising field, because on the whole doctors are not terribly good investigators. For example, none of the drugs developed for Alzheimers have worked at all, which suggests that our ideas on the causation of Alzheimers are likely wrong. Which suggests that it may (repeat may) be possible to make good progress on Alzheimers, either by an entirely empirical approach, which is way underrated nowadays, or by dumping the current explanation, finding a better one, and applying it.

You could start by looking at basic notions of field X and asking yourself: How do we really know that? Is there serious statistical evidence? Does that notion even accord with basic theory? This sort of checking is entirely possible. In most of the social sciences, we don’t, there isn’t, and it doesn’t.

Hygiene and the world distribution of Alzheimer’s disease: Epidemiological evidence for a relationship between microbial environment and age-adjusted disease burden: https://academic.oup.com/emph/article/2013/1/173/1861845/Hygiene-and-the-world-distribution-of-Alzheimer-s

Amyloid-β peptide protects against microbial infection in mouse and worm models of Alzheimer’s disease: http://stm.sciencemag.org/content/8/340/340ra72

Fungus, the bogeyman: http://www.economist.com/news/science-and-technology/21676754-curious-result-hints-possibility-dementia-caused-fungal

Fungus and dementia

paper: http://www.nature.com/articles/srep15015

Porphyromonas gingivalis in Alzheimer’s disease brains: Evidence for disease causation and treatment with small-molecule inhibitors: https://advances.sciencemag.org/content/5/1/eaau3333

july 2017 by nhaliday

Information Processing: Learn to solve every problem that has been solved

february 2017 by nhaliday

While it may be impossible to achieve Feynman's goal, I'm surprised that more people don't attempt the importance threshold-modified version. Suppose we set the importance bar really, really high: what are the most important results that everyone should try to understand? Here's a very biased partial list: basic physics and mathematics (e.g., to the level of the Feynman Lectures); quantitative theory of genetics and evolution; information, entropy and probability; basic ideas about logic and computation (Godel and Turing?); ... What else? Dynamics of markets? Complex Systems? Psychometrics? Descriptive biology? Organic chemistry?

hsu
scitariat
feynman
giants
stories
aphorism
curiosity
interdisciplinary
frontier
signal-noise
top-n
discussion
caltech
problem-solving
big-picture
vitality
🎓
virtu
big-surf
courage
🔬
allodium
nietzschean
ideas
quixotic
accretion
learning
hi-order-bits
february 2017 by nhaliday

Information Processing: Big, complicated data sets

february 2017 by nhaliday

This Times article profiles Nick Patterson, a mathematician whose career wandered from cryptography, to finance (7 years at Renaissance) and finally to bioinformatics. “I’m a data guy,” Dr. Patterson said. “What I know about is how to analyze big, complicated data sets.”

If you're a smart guy looking for something to do, there are 3 huge computational problems staring you in the face, for which the data is readily accessible.

1) human genome: 3 GB of data in a single genome; most data freely available on the Web (e.g., Hapmap stores patterns of sequence variation). Got a hypothesis about deep human history (evolution)? Test it yourself...

2) market prediction: every market tick available at zero or minimal subscription-service cost. Can you model short term movements? It's never been cheaper to build and test your model!

3) internet search: about 10^3 Terabytes of data (admittedly, a barrier to entry for an individual, but not for a startup). Can you come up with a better way to index or search it? What about peripheral problems like language translation or picture or video search?

The biggest barrier to entry is, of course, brainpower and a few years (a decade?) of concentrated learning. But the necessary books are all in the library :-)

Patterson has worked in 2 of the 3 areas listed above! Substituting crypto for internet search is understandable given his age, our cold war history, etc.

hsu
scitariat
quotes
links
news
org:rec
profile
giants
stories
huge-data-the-biggest
genomics
bioinformatics
finance
crypto
history
britain
interdisciplinary
the-trenches
🔬
questions
genetics
dataset
search
web
internet
scale
commentary
apollonian-dionysian
magnitude
examples
open-problems
big-surf
markets
securities
ORFE
nitty-gritty
quixotic
google
startups
ideas
measure
space-complexity
minimum-viable
move-fast-(and-break-things)
If you're a smart guy looking for something to do, there are 3 huge computational problems staring you in the face, for which the data is readily accessible.

1) human genome: 3 GB of data in a single genome; most data freely available on the Web (e.g., Hapmap stores patterns of sequence variation). Got a hypothesis about deep human history (evolution)? Test it yourself...

2) market prediction: every market tick available at zero or minimal subscription-service cost. Can you model short term movements? It's never been cheaper to build and test your model!

3) internet search: about 10^3 Terabytes of data (admittedly, a barrier to entry for an individual, but not for a startup). Can you come up with a better way to index or search it? What about peripheral problems like language translation or picture or video search?

The biggest barrier to entry is, of course, brainpower and a few years (a decade?) of concentrated learning. But the necessary books are all in the library :-)

Patterson has worked in 2 of the 3 areas listed above! Substituting crypto for internet search is understandable given his age, our cold war history, etc.

february 2017 by nhaliday

cc.complexity theory - Evidence that PPAD is hard? - Theoretical Computer Science Stack Exchange

q-n-a overflow tcs complexity algorithmic-econ game-theory motivation open-problems lower-bounds research relativization crypto rigorous-crypto nibble big-surf hardness questions equilibrium evidence

february 2017 by nhaliday

q-n-a overflow tcs complexity algorithmic-econ game-theory motivation open-problems lower-bounds research relativization crypto rigorous-crypto nibble big-surf hardness questions equilibrium evidence

february 2017 by nhaliday

computational complexity - Is P=NP relevant to finding proofs of everyday mathematical propositions? - MathOverflow

q-n-a overflow math meta:math tcs complexity interdisciplinary logic computation philosophy reflection gowers mathtariat nibble big-surf certificates-recognition

january 2017 by nhaliday

q-n-a overflow math meta:math tcs complexity interdisciplinary logic computation philosophy reflection gowers mathtariat nibble big-surf certificates-recognition

january 2017 by nhaliday

Shtetl-Optimized » Blog Archive » Logicians on safari

january 2017 by nhaliday

So what are they then? Maybe it’s helpful to think of them as “quantitative epistemology”: discoveries about the capacities of finite beings like ourselves to learn mathematical truths. On this view, the theoretical computer scientist is basically a mathematical logician on a safari to the physical world: someone who tries to understand the universe by asking what sorts of mathematical questions can and can’t be answered within it. Not whether the universe is a computer, but what kind of computer it is! Naturally, this approach to understanding the world tends to appeal most to people for whom math (and especially discrete math) is reasonably clear, whereas physics is extremely mysterious.

the sequel: http://www.scottaaronson.com/blog/?p=153

tcstariat
aaronson
tcs
computation
complexity
aphorism
examples
list
reflection
philosophy
multi
summary
synthesis
hi-order-bits
interdisciplinary
lens
big-picture
survey
nibble
org:bleg
applications
big-surf
s:*
p:whenever
ideas
elegance
the sequel: http://www.scottaaronson.com/blog/?p=153

january 2017 by nhaliday

ho.history overview - Proofs that require fundamentally new ways of thinking - MathOverflow

january 2017 by nhaliday

my favorite:

Although this has already been said elsewhere on MathOverflow, I think it's worth repeating that Gromov is someone who has arguably introduced more radical thoughts into mathematics than anyone else. Examples involving groups with polynomial growth and holomorphic curves have already been cited in other answers to this question. I have two other obvious ones but there are many more.

I don't remember where I first learned about convergence of Riemannian manifolds, but I had to laugh because there's no way I would have ever conceived of a notion. To be fair, all of the groundwork for this was laid out in Cheeger's thesis, but it was Gromov who reformulated everything as a convergence theorem and recognized its power.

Another time Gromov made me laugh was when I was reading what little I could understand of his book Partial Differential Relations. This book is probably full of radical ideas that I don't understand. The one I did was his approach to solving the linearized isometric embedding equation. His radical, absurd, but elementary idea was that if the system is sufficiently underdetermined, then the linear partial differential operator could be inverted by another linear partial differential operator. Both the statement and proof are for me the funniest in mathematics. Most of us view solving PDE's as something that requires hard work, involving analysis and estimates, and Gromov manages to do it using only elementary linear algebra. This then allows him to establish the existence of isometric embedding of Riemannian manifolds in a wide variety of settings.

q-n-a
overflow
soft-question
big-list
math
meta:math
history
insight
synthesis
gowers
mathtariat
hi-order-bits
frontier
proofs
magnitude
giants
differential
geometry
limits
flexibility
nibble
degrees-of-freedom
big-picture
novelty
zooming
big-surf
wild-ideas
metameta
courage
convergence
ideas
innovation
the-trenches
discovery
creative
elegance
Although this has already been said elsewhere on MathOverflow, I think it's worth repeating that Gromov is someone who has arguably introduced more radical thoughts into mathematics than anyone else. Examples involving groups with polynomial growth and holomorphic curves have already been cited in other answers to this question. I have two other obvious ones but there are many more.

I don't remember where I first learned about convergence of Riemannian manifolds, but I had to laugh because there's no way I would have ever conceived of a notion. To be fair, all of the groundwork for this was laid out in Cheeger's thesis, but it was Gromov who reformulated everything as a convergence theorem and recognized its power.

Another time Gromov made me laugh was when I was reading what little I could understand of his book Partial Differential Relations. This book is probably full of radical ideas that I don't understand. The one I did was his approach to solving the linearized isometric embedding equation. His radical, absurd, but elementary idea was that if the system is sufficiently underdetermined, then the linear partial differential operator could be inverted by another linear partial differential operator. Both the statement and proof are for me the funniest in mathematics. Most of us view solving PDE's as something that requires hard work, involving analysis and estimates, and Gromov manages to do it using only elementary linear algebra. This then allows him to establish the existence of isometric embedding of Riemannian manifolds in a wide variety of settings.

january 2017 by nhaliday

ds.algorithms - Evidence that matrix multiplication can be done in quadratic time? - Theoretical Computer Science Stack Exchange

q-n-a overflow tcs complexity algorithms linear-algebra algebraic-complexity motivation open-problems research frontier curiosity liner-notes math.GR alg-combo nibble big-surf questions

january 2017 by nhaliday

q-n-a overflow tcs complexity algorithms linear-algebra algebraic-complexity motivation open-problems research frontier curiosity liner-notes math.GR alg-combo nibble big-surf questions

january 2017 by nhaliday

Shtetl-Optimized » Blog Archive » Avi Wigderson’s “Permanent” Impact on Me

algebraic-complexity complexity aaronson talks tcs reflection synthesis tcstariat big-picture wigderson valiant sampling quantum quantum-info hierarchy counting nibble org:bleg big-surf essay p:whenever

october 2016 by nhaliday

algebraic-complexity complexity aaronson talks tcs reflection synthesis tcstariat big-picture wigderson valiant sampling quantum quantum-info hierarchy counting nibble org:bleg big-surf essay p:whenever

october 2016 by nhaliday

The probabilistic heuristic justification of the ABC conjecture | What's new

open-problems gowers thinking tricks intuition probability math tidbits yoga mathtariat models heuristic math.NT cartoons nibble org:bleg borel-cantelli big-surf additive multiplicative questions guessing

october 2016 by nhaliday

open-problems gowers thinking tricks intuition probability math tidbits yoga mathtariat models heuristic math.NT cartoons nibble org:bleg borel-cantelli big-surf additive multiplicative questions guessing

october 2016 by nhaliday

Ten Semi-Grand Challenges for Quantum Computing Theory

open-problems research expert list quantum tcs aaronson quantum-info tcstariat frontier top-n learning-theory deep-learning circuits crypto rigorous-crypto computation proof-systems big-surf questions ideas expert-experience quixotic

august 2016 by nhaliday

open-problems research expert list quantum tcs aaronson quantum-info tcstariat frontier top-n learning-theory deep-learning circuits crypto rigorous-crypto computation proof-systems big-surf questions ideas expert-experience quixotic

august 2016 by nhaliday

Principles of Effective Research | Michael Nielsen

productivity career academia grad-school advice expert strategy essay reflection phd long-term growth 🎓 learning aphorism len:long metabuch scholar tactics michael-nielsen tcstariat success habit big-picture org:bleg unit nibble meta:research metameta wire-guided big-surf skeleton gtd p:whenever s:*** hi-order-bits info-dynamics expert-experience problem-solving discipline grokkability-clarity ends-means telos-atelos time-use quantified-self integrity creative things questions cost-benefit certificates-recognition impetus motivation

july 2016 by nhaliday

productivity career academia grad-school advice expert strategy essay reflection phd long-term growth 🎓 learning aphorism len:long metabuch scholar tactics michael-nielsen tcstariat success habit big-picture org:bleg unit nibble meta:research metameta wire-guided big-surf skeleton gtd p:whenever s:*** hi-order-bits info-dynamics expert-experience problem-solving discipline grokkability-clarity ends-means telos-atelos time-use quantified-self integrity creative things questions cost-benefit certificates-recognition impetus motivation

july 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

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

Copy this bookmark: