nhaliday + msr   8

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
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

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 
january 2016 by nhaliday

bundles : academe

related tags

2016-election  academia  acm  algorithms  alt-inst  arrows  automata-languages  business  c(pp)  CAS  cjones-like  comparison  composition-decomposition  computational-geometry  convexity-curvature  cost-benefit  counter-revolution  critique  cs  curvature  discussion  dotnet  DSL  ecosystem  europe  expert-experience  formal-methods  frontier  functional  germanic  google  grokkability  hci  heavyweights  history  homepage  ideas  inference  innovation  institutions  interdisciplinary  intersection  intersection-connectedness  intricacy  language  learning  live-coding  machine-learning  math  math.CO  math.MG  math.NT  mathtariat  measure  meta:science  metric-space  metrics  microsoft  mostly-modern  msr  multi  nibble  nitty-gritty  nlp  ocaml-sml  organization  overflow  papers  pdf  people  performance  pls  plt  policy  positivity  prof  programming  proofs  proposal  q-n-a  questions  rant  reduction  repo  research  research-program  review  rigor  science  scitariat  security  signum  similarity  skunkworks  social-science  software  state-of-art  sublinear  survey  syntax  tcstariat  technology  the-trenches  the-world-is-just-atoms  tidbits  tools  tradeoffs  trump  types  usa  ux  west-hunter  worrydream 

Copy this bookmark: