nhaliday + proofs   97

The Future of Mathematics? [video] | Hacker News
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 
5 weeks ago by nhaliday
The Existential Risk of Math Errors - Gwern.net
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:


“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":

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.

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:


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.


more on formal methods in programming:

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 
july 2019 by nhaliday
What's the expected level of paper for top conferences in Computer Science - Academia Stack Exchange
Top. The top level.

My experience on program committees for STOC, FOCS, ITCS, SODA, SOCG, etc., is that there are FAR more submissions of publishable quality than can be accepted into the conference. By "publishable quality" I mean a well-written presentation of a novel, interesting, and non-trivial result within the scope of the conference.


There are several questions that come up over and over in the FOCS/STOC review cycle:

- How surprising / novel / elegant / interesting is the result?
- How surprising / novel / elegant / interesting / general are the techniques?
- How technically difficult is the result? Ironically, FOCS and STOC committees have a reputation for ignoring the distinction between trivial (easy to derive from scratch) and nondeterministically trivial (easy to understand after the fact).
- What is the expected impact of this result? Is this paper going to change the way people do theoretical computer science over the next five years?
- Is the result of general interest to the theoretical computer science community? Or is it only of interest to a narrow subcommunity? In particular, if the topic is outside the STOC/FOCS mainstream—say, for example, computational topology—does the paper do a good job of explaining and motivating the results to a typical STOC/FOCS audience?
nibble  q-n-a  overflow  academia  tcs  cs  meta:research  publishing  scholar  lens  properties  cost-benefit  analysis  impetus  increase-decrease  soft-question  motivation  proofs  search  complexity  analogy  problem-solving  elegance  synthesis  hi-order-bits  novelty  discovery 
june 2019 by nhaliday
gn.general topology - Pair of curves joining opposite corners of a square must intersect---proof? - MathOverflow
In his 'Ordinary Differential Equations' (sec. 1.2) V.I. Arnold says "... every pair of curves in the square joining different pairs of opposite corners must intersect".

This is obvious geometrically but I was wondering how one could go about proving this rigorously. I have thought of a proof using Brouwer's Fixed Point Theorem which I describe below. I would greatly appreciate the group's comments on whether this proof is right and if a simpler proof is possible.


Since the full Jordan curve theorem is quite subtle, it might be worth pointing out that theorem in question reduces to the Jordan curve theorem for polygons, which is easier.

Suppose on the contrary that the curves A,BA,B joining opposite corners do not meet. Since A,BA,B are closed sets, their minimum distance apart is some ε>0ε>0. By compactness, each of A,BA,B can be partitioned into finitely many arcs, each of which lies in a disk of diameter <ε/3<ε/3. Then, by a homotopy inside each disk we can replace A,BA,B by polygonal paths A′,B′A′,B′ that join the opposite corners of the square and are still disjoint.

Also, we can replace A′,B′A′,B′ by simple polygonal paths A″,B″A″,B″ by omitting loops. Now we can close A″A″ to a polygon, and B″B″ goes from its "inside" to "outside" without meeting it, contrary to the Jordan curve theorem for polygons.

- John Stillwell
nibble  q-n-a  overflow  math  geometry  topology  tidbits  intricacy  intersection  proofs  gotchas  oly  mathtariat  fixed-point  math.AT  manifolds  intersection-connectedness 
october 2017 by nhaliday
Section 10 Chi-squared goodness-of-fit test.
- pf that chi-squared statistic for Pearson's test (multinomial goodness-of-fit) actually has chi-squared distribution asymptotically
- the gotcha: terms Z_j in sum aren't independent
- solution:
- compute the covariance matrix of the terms to be E[Z_iZ_j] = -sqrt(p_ip_j)
- note that an equivalent way of sampling the Z_j is to take a random standard Gaussian and project onto the plane orthogonal to (sqrt(p_1), sqrt(p_2), ..., sqrt(p_r))
- that is equivalent to just sampling a Gaussian w/ 1 less dimension (hence df=r-1)
pdf  nibble  lecture-notes  mit  stats  hypothesis-testing  acm  probability  methodology  proofs  iidness  distribution  limits  identity  direction  lifts-projections 
october 2017 by nhaliday
self study - Looking for a good and complete probability and statistics book - Cross Validated
I never had the opportunity to visit a stats course from a math faculty. I am looking for a probability theory and statistics book that is complete and self-sufficient. By complete I mean that it contains all the proofs and not just states results.
nibble  q-n-a  overflow  data-science  stats  methodology  books  recommendations  list  top-n  confluence  proofs  rigor  reference  accretion 
october 2017 by nhaliday
newtonian gravity - Newton's original proof of gravitation for non-point-mass objects - Physics Stack Exchange
This theorem is Proposition LXXI, Theorem XXXI in the Principia. To warm up, consider the more straightforward proof of the preceding theorem, that there's no inverse-square force inside of a spherical shell:


The crux of the argument is that the triangles HPI and LPK are similar. The mass enclosed in the small-but-near patch of sphere HI goes like the square of the distance HP, while the mass enclosed in the large-but-far patch of sphere KL, with the same solid angle, goes like the square of the distance KP. This mass ratio cancels out the distance-squared ratio governing the strength of the force, and so the net force from those two patches vanishes.

For a point mass outside a shell, Newton's approach is essentially the same as the modern approach:


One integral is removed because we're considering a thin spherical shell rather than a solid sphere. The second integral, "as the semi-circle AKB revolves about the diameter AB," trivially turns Newton's infinitesimal arcs HI and KL into annuli.

The third integral is over all the annuli in the sphere, over 0≤ϕ≤τ/20≤ϕ≤τ/2 or over R−r≤s≤R+rR−r≤s≤R+r. This one is a little bit hairy, even with the advantage of modern notation.

Newton's clever trick is to consider the relationship between the force due to the smaller, nearer annulus HI and the larger, farther annulus KL defined by the same viewing angle (in modern notation, dθdθ). If I understand correctly he argues again, based on lots of similar triangles with infinitesimal angles, that the smaller-but-nearer annulus and the larger-but-farther annulus exert the same force at P. Furthermore, he shows that the force doesn't depend on the distance PF, and thus doesn't depend on the radius of the sphere; the only parameter left is the distance PS (squared) between the particle and the sphere's center. Since the argument doesn't depend on the angle HPS, it's true for all the annuli, and the theorem is proved.
nibble  q-n-a  overflow  giants  old-anglo  the-trenches  physics  mechanics  gravity  proofs  symmetry  geometry  spatial 
september 2017 by nhaliday
Inscribed angle - Wikipedia
- for triangle w/ one side = a diameter, draw isosceles triangle and use supplementary angle identities
- otherwise draw second triangle w/ side = a diameter, and use above result twice
nibble  math  geometry  spatial  ground-up  wiki  reference  proofs  identity  levers  yoga 
august 2017 by nhaliday
Subgradients - S. Boyd and L. Vandenberghe
If f is convex and x ∈ int dom f, then ∂f(x) is nonempty and bounded. To establish that ∂f(x) ≠ ∅, we apply the supporting hyperplane theorem to the convex set epi f at the boundary point (x, f(x)), ...
pdf  nibble  lecture-notes  acm  optimization  curvature  math.CA  estimate  linearity  differential  existence  proofs  exposition  atoms  math  marginal  convexity-curvature 
august 2017 by nhaliday
Roche limit - Wikipedia
In celestial mechanics, the Roche limit (pronounced /ʁɔʃ/) or Roche radius, is the distance within which a celestial body, held together only by its own gravity, will disintegrate due to a second celestial body's tidal forces exceeding the first body's gravitational self-attraction.[1] Inside the Roche limit, orbiting material disperses and forms rings whereas outside the limit material tends to coalesce. The term is named after Édouard Roche, who is the French astronomer who first calculated this theoretical limit in 1848.[2]
space  physics  gravity  mechanics  wiki  reference  nibble  phase-transition  proofs  tidbits  identity  marginal 
july 2017 by nhaliday
co.combinatorics - Classification of Platonic solids - MathOverflow
My question is very basic: where can I find a complete (and hopefully self-contained) proof of the classification of Platonic solids? In all the references that I found, they use Euler's formula v−e+f=2v−e+f=2 to show that there are exactly five possible triples (v,e,f)(v,e,f). But of course this is not a complete proof because it does not rule out the possibility of different configurations or deformations. Has anyone ever written up a complete proof of this statement?!


This is a classical question. Here is my reading of it: Why is there a unique polytope with given combinatorics of faces, which are all regular polygons? Of course, for simple polytopes (tetrahedron, cube, dodecahedron) this is clear, but for the octahedron and icosahedron this is less clear.

The answer lies in the Cauchy's theorem. It was Legendre, while writing his Elements of Geometry and Trigonometry, noticed that Euclid's proof is incomplete in the Elements. Curiously, Euclid finds both radii of inscribed and circumscribed spheres (correctly) without ever explaining why they exist. Cauchy worked out a proof while still a student in 1813, more or less specifically for this purpose. The proof also had a technical gap which was found and patched up by Steinitz in 1920s.

The complete (corrected) proof can be found in the celebrated Proofs from the Book, or in Marcel Berger's Geometry. My book gives a bit more of historical context and some soft arguments (ch. 19). It's worth comparing this proof with (an erroneous) pre-Steinitz exposition, say in Hadamard's Leçons de Géométrie Elémentaire II, or with an early post-Steinitz correct but tedious proof given in (otherwise, excellent) Alexandrov's monograph (see also ch.26 in my book which compares all the approaches).

P.S. Note that Coxeter in Regular Polytopes can completely avoid this issue but taking a different (modern) definition of the regular polytopes (which are symmetric under group actions). For a modern exposition and the state of art of this approach, see McMullen and Schulte's Abstract Regular Polytopes.

q-n-a  overflow  math  topology  geometry  math.CO  history  iron-age  mediterranean  the-classics  multi  curiosity  clarity  proofs  nibble  wiki  reference  characterization  uniqueness  list  ground-up  grokkability-clarity 
july 2017 by nhaliday
Lecture 6: Nash Equilibrum Existence
- For mixed strategy profile p ∈ Δ(A), let g_ij(p) = gain for player i to switch to pure strategy j.
- Define y: Δ(A) -> Δ(A) by y_ij(p) ∝ p_ij + g_ij(p) (normalizing constant = 1 + ∑_k g_ik(p)).
- Look at fixed point of y.
pdf  nibble  lecture-notes  exposition  acm  game-theory  proofs  math  topology  existence  fixed-point  simplex  equilibrium  ground-up 
june 2017 by nhaliday
Redistributing from Capitalists to Workers: An Impossibility Theorem, Garett Jones | EconLog | Library of Economics and Liberty
org:econlib  econotariat  spearhead  garett-jones  economics  policy  rhetoric  thinking  analysis  no-go  redistribution  labor  taxes  cracker-econ  multi  piketty  news  org:lite  org:biz  pdf  links  political-econ  capital  simulation  operational  dynamic  explanation  time-preference  patience  wonkish  study  science-anxiety  externalities  long-short-run  models  map-territory  stylized-facts  s:*  broad-econ  chart  article  🎩  randy-ayndy  envy  bootstraps  inequality  absolute-relative  X-not-about-Y  volo-avolo  ideas  status  capitalism  nationalism-globalism  metabuch  optimate  aristos  open-closed  macro  government  proofs  equilibrium 
february 2017 by nhaliday
Hoeffding’s Inequality
basic idea of standard pf: bound e^{tX} by line segment (convexity) then use Taylor expansion (in p = b/(b-a), the fraction of range to right of 0) of logarithm
pdf  lecture-notes  exposition  nibble  concentration-of-measure  estimate  proofs  ground-up  acm  probability  series  s:null 
february 2017 by nhaliday
inequalities - Is the Jaccard distance a distance? - MathOverflow
Steinhaus Transform
the referenced survey: http://kenclarkson.org/nn_survey/p.pdf

It's known that this transformation produces a metric from a metric. Now if you take as the base metric D the symmetric difference between two sets, what you end up with is the Jaccard distance (which actually is known by many other names as well).
q-n-a  overflow  nibble  math  acm  sublinear  metrics  metric-space  proofs  math.CO  tcstariat  arrows  reduction  measure  math.MG  similarity  multi  papers  survey  computational-geometry  cs  algorithms  pdf  positivity  msr  tidbits  intersection  curvature  convexity-curvature  intersection-connectedness  signum 
february 2017 by nhaliday
Equivalence between counting and sampling
also: every counting problem either has FPTRAS or no approx. w/i polynomial factor
pdf  exposition  lecture-notes  berkeley  nibble  tcs  counting  sampling  characterization  complexity  approximation  rand-approx  proofs 
february 2017 by nhaliday
Structure theorem for finitely generated modules over a principal ideal domain - Wikipedia
- finitely generative modules over PID isomorphic to sum of quotients by decreasing sequences of proper ideals
- never really understood the proof of this in Ma5b
math  algebra  characterization  levers  math.AC  wiki  reference  nibble  proofs  additive  arrows 
february 2017 by nhaliday
bounds - What is the variance of the maximum of a sample? - Cross Validated
- sum of variances is always a bound
- can't do better even for iid Bernoulli
- looks like nice argument from well-known probabilist (using E[(X-Y)^2] = 2Var X), but not clear to me how he gets to sum_i instead of sum_{i,j} in the union bound?
edit: argument is that, for j = argmax_k Y_k, we have r < X_i - Y_j <= X_i - Y_i for all i, including i = argmax_k X_k
- different proof here (later pages): http://www.ism.ac.jp/editsec/aism/pdf/047_1_0185.pdf
Var(X_n:n) <= sum Var(X_k:n) + 2 sum_{i < j} Cov(X_i:n, X_j:n) = Var(sum X_k:n) = Var(sum X_k) = nσ^2
why are the covariances nonnegative? (are they?). intuitively seems true.
- for that, see https://pinboard.in/u:nhaliday/b:ed4466204bb1
- note that this proof shows more generally that sum Var(X_k:n) <= sum Var(X_k)
- apparently that holds for dependent X_k too? http://mathoverflow.net/a/96943/20644
q-n-a  overflow  stats  acm  distribution  tails  bias-variance  moments  estimate  magnitude  probability  iidness  tidbits  concentration-of-measure  multi  orders  levers  extrema  nibble  bonferroni  coarse-fine  expert  symmetry  s:*  expert-experience  proofs 
february 2017 by nhaliday
A brief philosophical discussion:
Measure theory, as much as any branch of mathematics, is an area where it is important to be acquainted with the basic notions and statements, but not desperately important to be acquainted with the detailed proofs, which are often rather unilluminating. One should always have in a mind a place where one could go and look if one ever did need to understand a proof: for me, that place is Rudin’s Real and Complex Analysis (Rudin’s “red book”).
gowers  pdf  math  math.CA  math.FA  philosophy  measure  exposition  synthesis  big-picture  hi-order-bits  ergodic  ground-up  summary  roadmap  mathtariat  proofs  nibble  unit  integral  zooming  p:whenever 
february 2017 by nhaliday
Could I be using proof by contradiction too much? - Mathematics Stack Exchange
One general reason to avoid proof by contradiction is the following. When you prove something by contradiction, all you learn is that the statement you wanted to prove is true. When you prove something directly, you learn every intermediate implication you had to prove along the way.
q-n-a  overflow  math  proofs  contradiction  oly  mathtariat  nibble 
february 2017 by nhaliday
electromagnetism - Is Biot-Savart law obtained empirically or can it be derived? - Physics Stack Exchange
Addendum: In mathematics and science it is important to keep in mind the distinction between the historical and the logical development of a subject. Knowing the history of a subject can be useful to get a sense of the personalities involved and sometimes to develop an intuition about the subject. The logical presentation of the subject is the way practitioners think about it. It encapsulates the main ideas in the most complete and simple fashion. From this standpoint, electromagnetism is the study of Maxwell's equations and the Lorentz force law. Everything else is secondary, including the Biot-Savart law.
q-n-a  overflow  physics  electromag  synthesis  proofs  nibble 
february 2017 by nhaliday
Cauchy-Schwarz inequality and Hölder's inequality - Mathematics Stack Exchange
- Cauchy-Schwarz (special case of Holder's inequality where p=q=1/2) implies Holder's inequality
- pith: define potential F(t) = int f^{pt} g^{q(1-t)}, show log F is midpoint-convex hence convex, then apply convexity between F(0) and F(1) for F(1/p) = ||fg||_1
q-n-a  overflow  math  estimate  proofs  ground-up  math.FA  inner-product  tidbits  norms  duality  nibble  integral 
january 2017 by nhaliday
5/8 bound in group theory - MathOverflow
very elegant proof (remember sum d_i^2 = |G| and # irreducible rep.s = # conjugacy classes)
q-n-a  overflow  math  tidbits  proofs  math.RT  math.GR  oly  commutativity  pigeonhole-markov  nibble  shift 
january 2017 by nhaliday
Dvoretzky's theorem - Wikipedia
In mathematics, Dvoretzky's theorem is an important structural theorem about normed vector spaces proved by Aryeh Dvoretzky in the early 1960s, answering a question of Alexander Grothendieck. In essence, it says that every sufficiently high-dimensional normed vector space will have low-dimensional subspaces that are approximately Euclidean. Equivalently, every high-dimensional bounded symmetric convex set has low-dimensional sections that are approximately ellipsoids.

math  math.FA  inner-product  levers  characterization  geometry  math.MG  concentration-of-measure  multi  q-n-a  overflow  intuition  examples  proofs  dimensionality  gowers  mathtariat  tcstariat  quantum  quantum-info  norms  nibble  high-dimension  wiki  reference  curvature  convexity-curvature  tcs 
january 2017 by nhaliday
probability - How to prove Bonferroni inequalities? - Mathematics Stack Exchange
- integrated version of inequalities for alternating sums of (N choose j), where r.v. N = # of events occuring
- inequalities for alternating binomial coefficients follow from general property of unimodal (increasing then decreasing) sequences, which can be gotten w/ two cases for increasing and decreasing resp.
- the final alternating zero sum property follows for binomial coefficients from expanding (1 - 1)^N = 0
- The idea of proving inequality by integrating simpler inequality of r.v.s is nice. Proof from CS 150 was more brute force from what I remember.
q-n-a  overflow  math  probability  tcs  probabilistic-method  estimate  proofs  levers  yoga  multi  tidbits  metabuch  monotonicity  calculation  nibble  bonferroni  tricki  binomial  s:null  elegance 
january 2017 by nhaliday
In Computers We Trust? | Quanta Magazine
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  technical-writing  trust 
january 2017 by nhaliday
ho.history overview - Proofs that require fundamentally new ways of thinking - MathOverflow
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 
january 2017 by nhaliday
« earlier      
per page:    204080120160

bundles : academemathmetaproblem-solving

related tags

aaronson  absolute-relative  abstraction  academia  accretion  acm  acmtariat  additive  additive-combo  advanced  aesthetics  agri-mindset  ai  algebra  algebraic-complexity  algorithms  amortization-potential  AMT  analogy  analysis  announcement  aphorism  applications  approximation  aristos  arrows  article  atoms  automation  bare-hands  bayesian  beauty  berkeley  better-explained  bias-variance  big-list  big-picture  big-surf  binomial  bio  bits  boltzmann  bonferroni  books  boolean-analysis  bootstraps  broad-econ  brunn-minkowski  c(pp)  calculation  caltech  capital  capitalism  cartoons  CAS  certificates-recognition  characterization  chart  cheatsheet  checking  circuits  clarity  clever-rats  coarse-fine  cocktail  coding-theory  collaboration  coloring  combo-optimization  commentary  communication  commutativity  comparison  complexity  composition-decomposition  compressed-sensing  computation  computational-geometry  concentration-of-measure  concept  conceptual-vocab  concurrency  confluence  confusion  constraint-satisfaction  contradiction  contrarianism  convergence  convexity-curvature  correctness  cost-benefit  counting  coupling-cohesion  courage  course  cracker-econ  cracker-prog  creative  critique  cs  culture  curiosity  curvature  data-science  database  debate  decision-making  decision-theory  definition  degrees-of-freedom  dependence-independence  differential  dimensionality  direction  dirty-hands  discovery  discussion  distributed  distribution  documentation  DP  draft  DSL  duality  duplication  dynamic  dynamical  early-modern  economics  econotariat  ecosystem  education  efficiency  electromag  elegance  embeddings  emergent  encyclopedic  ends-means  engineering  entropy-like  envy  epistemic  equilibrium  ergodic  error  essay  estimate  europe  examples  existence  exocortex  expectancy  experiment  expert  expert-experience  explanation  exposition  externalities  extrema  features  fields  fixed-point  flexibility  fluid  flux-stasis  formal-methods  formal-values  frontier  functional  game-theory  garett-jones  genetics  geometry  giants  git  gnxp  gotchas  government  gowers  graph-theory  graphs  gravity  greedy  grokkability  grokkability-clarity  ground-up  guessing  gwern  hardness  haskell  heavyweights  heuristic  hi-order-bits  high-dimension  higher-ed  history  hmm  hn  homogeneity  hypothesis-testing  ideas  identity  iidness  impetus  increase-decrease  induction  inequality  inference  info-dynamics  information-theory  inner-product  innovation  insight  integral  interdisciplinary  intersection  intersection-connectedness  intricacy  intuition  invariance  iron-age  iteration-recursion  knowledge  labor  learning  lecture-notes  lectures  lens  levers  lifts-projections  limits  linear-algebra  linearity  liner-notes  links  list  local-global  logic  long-short-run  lower-bounds  luca-trevisan  machine-learning  macro  magnitude  manifolds  map-territory  marginal  markov  math  math.AC  math.AG  math.AT  math.CA  math.CO  math.CT  math.CV  math.DS  math.FA  math.GN  math.GR  math.MG  math.NT  math.RT  mathtariat  matrix-factorization  measure  mechanics  mediterranean  meta:math  meta:prediction  meta:research  metabuch  metameta  methodology  metric-space  metrics  michael-nielsen  micro  minimalism  miri-cfar  mit  models  moments  monotonicity  monte-carlo  motivation  move-fast-(and-break-things)  msr  multi  multiplicative  narrative  nationalism-globalism  naturality  necessity-sufficiency  news  nibble  nitty-gritty  no-go  nonlinearity  norms  novelty  objektbuch  occam  old-anglo  oly  online-learning  open-closed  open-problems  operational  optimate  optimism  optimization  orders  ORFE  org:biz  org:bleg  org:econlib  org:edu  org:inst  org:junk  org:lite  org:mag  org:mat  org:sci  oscillation  oss  outcome-risk  outliers  overflow  p:someday  p:whenever  PAC  papers  parsimony  patience  PCP  pdf  phase-transition  philosophy  physics  pic  pigeonhole-markov  piketty  plots  pls  plt  policy  political-econ  polynomials  popsci  population-genetics  positivity  pragmatic  prediction  preprint  presentation  princeton  probabilistic-method  probability  problem-solving  programming  proof-systems  proofs  properties  pseudorandomness  publishing  puzzles  python  q-n-a  qra  quantifiers-sums  quantum  quantum-info  questions  rand-approx  random  randy-ayndy  ratty  realness  reason  recommendations  redistribution  reduction  reference  reflection  relativization  replication  research  research-program  review  rhetoric  rigidity  rigor  risk  roadmap  robust  s:*  s:**  s:***  s:null  sampling  sanjeev-arora  scale  scholar  science-anxiety  scitariat  SDP  search  sensitivity  series  shift  signum  similarity  simplex  simplification-normalization  simulation  skeleton  skunkworks  slides  smoothness  soft-question  software  space  span-cover  sparsity  spatial  spearhead  spectral  speculation  stackex  stanford  stat-mech  state-of-art  static-dynamic  stats  status  stories  street-fighting  structure  study  stylized-facts  sublinear  summary  survey  symmetry  synchrony  synthesis  system-design  systematic-ad-hoc  tails  talks  taxes  tcs  tcstariat  teaching  technical-writing  techtariat  temperature  tensors  the-classics  the-trenches  thermo  thesis  thinking  threat-modeling  thurston  tidbits  tightness  time-complexity  time-preference  tip-of-tongue  toolkit  tools  top-n  topology  track-record  tradeoffs  tricki  tricks  trivia  trust  truth  types  UGC  uniqueness  unit  vague  values  vcs  video  virtu  visual-understanding  visualization  volo-avolo  von-neumann  waves  wigderson  wiki  wild-ideas  wisdom  wonkish  wormholes  worrydream  worse-is-better/the-right-thing  writing  X-not-about-Y  yoga  zooming  🎓  🎩  👳 

Copy this bookmark: