nhaliday + math.nt   51

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
Factorization of polynomials over finite fields - Wikipedia
In mathematics and computer algebra the factorization of a polynomial consists of decomposing it into a product of irreducible factors. This decomposition is theoretically possible and is unique for polynomials with coefficients in any field, but rather strong restrictions on the field of the coefficients are needed to allow the computation of the factorization by means of an algorithm. In practice, algorithms have been designed only for polynomials with coefficients in a finite field, in the field of rationals or in a finitely generated field extension of one of them.

All factorization algorithms, including the case of multivariate polynomials over the rational numbers, reduce the problem to this case; see polynomial factorization. It is also used for various applications of finite fields, such as coding theory (cyclic redundancy codes and BCH codes), cryptography (public key cryptography by the means of elliptic curves), and computational number theory.

As the reduction of the factorization of multivariate polynomials to that of univariate polynomials does not have any specificity in the case of coefficients in a finite field, only polynomials with one variable are considered in this article.


In the algorithms that follow, the complexities are expressed in terms of number of arithmetic operations in Fq, using classical algorithms for the arithmetic of polynomials.

[ed.: Interesting choice...]


Factoring algorithms
Many algorithms for factoring polynomials over finite fields include the following three stages:

Square-free factorization
Distinct-degree factorization
Equal-degree factorization
An important exception is Berlekamp's algorithm, which combines stages 2 and 3.

Berlekamp's algorithm
Main article: Berlekamp's algorithm
The Berlekamp's algorithm is historically important as being the first factorization algorithm, which works well in practice. However, it contains a loop on the elements of the ground field, which implies that it is practicable only over small finite fields. For a fixed ground field, its time complexity is polynomial, but, for general ground fields, the complexity is exponential in the size of the ground field.

[ed.: This actually looks fairly implementable.]
wiki  reference  concept  algorithms  calculation  nibble  numerics  math  algebra  math.CA  fields  polynomials  levers  multiplicative  math.NT 
july 2019 by nhaliday
About - Project Euler
I've written my program but should it take days to get to the answer?
Absolutely not! Each problem has been designed according to a "one-minute rule", which means that although it may take several hours to design a successful algorithm with more difficult problems, an efficient implementation will allow a solution to be obtained on a modestly powered computer in less than one minute.
math  rec-math  math.NT  math.CO  programming  oly  database  community  forum  stream  problem-solving  accretion  puzzles  contest  🖥  👳 
june 2019 by nhaliday
Diophantine approximation - Wikipedia
- rationals perfectly approximated by themselves, badly approximated (eps>1/bq) by other rationals
- irrationals well-approximated (eps~1/q^2) by rationals:
nibble  wiki  reference  math  math.NT  approximation  accuracy  levers  pigeonhole-markov  multi  tidbits  discrete  rounding  estimate  tightness  algebra 
august 2017 by nhaliday
Main Page - Competitive Programming Algorithms: E-Maxx Algorithms in English
original russian version: http://e-maxx.ru/algo/

some notable stuff:
- O(N) factorization sieve
- discrete logarithm
- factorial N! (mod P) in O(P log N)
- flow algorithms
- enumerating submasks
- bridges, articulation points
- Ukkonen algorithm
- sqrt(N) trick, eg, for range mode query
explanation  programming  algorithms  russia  foreign-lang  oly  oly-programming  problem-solving  accretion  math.NT  graphs  graph-theory  optimization  data-structures  yoga  tidbits  multi  anglo  language  arrows  strings 
february 2017 by nhaliday
254A, Supplement 4: Probabilistic models and heuristics for the primes (optional) | What's new
among others, the Cramér model for the primes (basically kinda looks like primality is independently distributed w/ Pr[n is prime] = 1/log n)
gowers  mathtariat  lecture-notes  exposition  math  math.NT  probability  heuristic  models  cartoons  nibble  org:bleg  pseudorandomness  borel-cantelli  concentration-of-measure  multiplicative  truth  guessing 
february 2017 by nhaliday
nt.number theory - Is $x^{2k+1} - 7x^2 + 1$ irreducible? - MathOverflow
Here is a proof, based on a trick that can be used to prove that x^n+x+1 is irreducible when n≠2 mod 3.
q-n-a  overflow  math  algebra  tidbits  math.NT  contradiction  polynomials  nibble  multiplicative 
january 2017 by nhaliday
The Mathematician Ken Ono’s Life Inspired By Ramanujan | Quanta Magazine
This intellectual crucible produced the desired results — Ono studied mathematics and launched a promising academic career — but at great emotional cost. As a teenager, Ono became so desperate to escape his parents’ expectations that he dropped out of high school. He later earned admission to the University of Chicago but had an apathetic attitude toward his studies, preferring to party with his fraternity brothers. He eventually discovered a genuine enthusiasm for mathematics, became a professor, and started a family, but fear of failure still weighed so heavily on Ono that he attempted suicide while attending an academic conference. Only after he joined the Institute for Advanced Study himself did Ono begin to make peace with his upbringing.
profile  math  people  career  popsci  hmm  news  org:mag  org:sci  giants  math.NT  nibble  org:inst  heavyweights 
may 2016 by nhaliday
The goal of the Lean Forward project is to collaborate with number theorists to formally prove theorems about research mathematics and to address the main usability issues hampering the adoption of proof assistants in mathematical circles. The theorems will be selected together with our collaborators to guide the development of formal libraries and verified tools.

mostly happening in the Netherlands


A Review of the Lean Theorem Prover: https://jiggerwit.wordpress.com/2018/09/18/a-review-of-the-lean-theorem-prover/
- Thomas Hales
seems like a Coq might be a better starter if I ever try to get into proof assistants/theorem provers

edit: on second thought this actually seems like a wash for beginners

An Argument for Controlled Natural Languages in Mathematics: https://jiggerwit.wordpress.com/2019/06/20/an-argument-for-controlled-natural-languages-in-mathematics/
By controlled natural language for mathematics (CNL), we mean an artificial language for the communication of mathematics that is (1) designed in a deliberate and explicit way with precise computer-readable syntax and semantics, (2) based on a single natural language (such as Chinese, Spanish, or English), and (3) broadly understood at least in an intuitive way by mathematically literate speakers of the natural language.

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

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

research  math  formal-methods  msr  multi  homepage  research-program  skunkworks  math.NT  academia  ux  CAS  mathtariat  expert-experience  cost-benefit  nitty-gritty  review  critique  rant  types  learning  intricacy  functional  performance  c(pp)  ocaml-sml  comparison  ecosystem  DSL  tradeoffs  composition-decomposition  interdisciplinary  europe  germanic  grokkability  nlp  language  heavyweights  inference  rigor  automata-languages  repo  software  tools  syntax  frontier  state-of-art  pls  grokkability-clarity  technical-writing  database  lifts-projections 
january 2016 by nhaliday

bundles : academeframemath

related tags

aaronson  academia  accretion  accuracy  acm  additive  additive-combo  advanced  aesthetics  alg-combo  algebra  algebraic-complexity  algorithms  AMT  anglo  announcement  applications  approximation  arrows  automata-languages  automation  bayesian  beauty  better-explained  big-list  big-picture  big-surf  binomial  bio  blowhards  books  boolean-analysis  borel-cantelli  business  c(pp)  calculation  career  cartoons  CAS  characterization  chart  cheatsheet  checking  checklists  chemistry  circuits  clarity  clever-rats  coding-theory  cog-psych  commentary  communication  communication-complexity  community  comparison  complexity  composition-decomposition  concentration-of-measure  concept  conceptual-vocab  confluence  contest  contradiction  convexity-curvature  cool  correctness  cost-benefit  counterexample  coupling-cohesion  course  criminal-justice  critique  crosstab  crypto  cs  curiosity  curvature  data-science  data-structures  database  dataviz  dbs  debugging  decision-making  decision-theory  definition  degrees-of-freedom  differential  discrete  discussion  documentation  dotnet  DP  DSL  dynamic  economics  ecosystem  editors  education  efficiency  electromag  elegance  embeddings  epistemic  erdos  error  estimate  ethics  europe  examples  exocortex  experiment  expert  expert-experience  explanation  exposition  extratricky  feynman  fields  film  finiteness  foreign-lang  formal-methods  formal-values  forum  fourier  frontier  functional  game-theory  geometry  germanic  giants  git  golang  gowers  graph-theory  graphs  greedy  grokkability  grokkability-clarity  ground-up  growth  GT-101  guessing  hamming  harvard  haskell  heavyweights  heuristic  hg  hi-order-bits  higher-ed  history  hmm  hn  homepage  howto  ideas  identity  idk  IEEE  impetus  impro  induction  inference  info-foraging  information-theory  init  insight  integral  interdisciplinary  interview  intricacy  intuition  iteration-recursion  javascript  jvm  knowledge  language  learning  lecture-notes  lens  lesswrong  letters  levers  libraries  lifts-projections  linear-algebra  linear-programming  links  lisp  list  logic  machine-learning  macro  magnitude  markov  math  math.AG  math.CA  math.CO  math.CV  math.DS  math.FA  math.GR  math.NT  math.RT  mathtariat  measure  measurement  mental-math  meta:research  metabuch  metameta  methodology  michael-nielsen  micro  minimalism  mit  models  monte-carlo  mostly-modern  motivation  msr  multi  multiplicative  music-theory  naturality  nature  necessity-sufficiency  neuro  news  nibble  nitty-gritty  nlp  numerics  objektbuch  ocaml-sml  occam  oly  oly-programming  oop  open-problems  optimism  optimization  org:bleg  org:inst  org:mag  org:mat  org:sci  orourke  overflow  oxbridge  p:**  p:someday  p:whenever  papers  parsimony  pdf  people  performance  philosophy  physics  pigeonhole-markov  plots  pls  plt  polynomials  popsci  pre-2013  prediction  presentation  prioritizing  probabilistic-method  probability  problem-solving  prof  profile  programming  proofs  pseudorandomness  psychology  puzzles  python  q-n-a  qra  quantum  questions  quixotic  r-lang  rand-approx  random  rant  rationality  ratty  reading  rec-math  recommendations  reference  reflection  relativity  repo  research  research-program  review  rhetoric  rigor  rigorous-crypto  rounding  russia  rust  s:*  s:***  salil-vadhan  scala  sci-comp  search  simplification-normalization  skeleton  skunkworks  slides  smoothness  social-science  soft-question  software  space-complexity  span-cover  spectral  speculation  stackex  stanford  stat-mech  state-of-art  static-dynamic  stats  stories  stream  street-fighting  strings  structure  subculture  summary  syntax  synthesis  talks  tcs  tcstariat  teaching  technical-writing  techtariat  terminal  the-trenches  thermo  thinking  tidbits  tightness  time-complexity  tools  top-n  topics  topology  track-record  tradeoffs  tricki  tricks  trivia  trust  truth  tutorial  types  unit  unix  ux  vague  valiant  vcs  video  volo-avolo  whole-partial-many  wigderson  wiki  world-war  wormholes  yoga  👳  🖥  🤖  🦉 

Copy this bookmark: