**nhaliday + heavyweights + expert-experience**
16

CppCon 2015: Chandler Carruth "Tuning C++: Benchmarks, and CPUs, and Compilers! Oh My!" - YouTube

8 days ago by nhaliday

- very basics of benchmarking

- Q: why does preemptive reserve speed up push_back by 10x?

- favoriate tool is Linux perf

- callgraph profiling

- important option: -fomit-frame-pointer

- perf has nice interface ('a' = "annotate") for reading assembly (good display of branches/jumps)

- A: optimized to no-op

- how to turn off optimizer

- profilers aren't infallible. a lot of the time samples are misattributed to neighboring ops

- fast mod example

- branch prediction hints (#define UNLIKELY(x), __builtin_expected, etc)

video
presentation
c(pp)
pls
programming
unix
heavyweights
cracker-prog
benchmarks
engineering
best-practices
working-stiff
systems
expert-experience
google
llvm
common-case
stories
libraries
measurement
linux
performance
traces
graphs
static-dynamic
ui
assembly
compilers
methodology
- Q: why does preemptive reserve speed up push_back by 10x?

- favoriate tool is Linux perf

- callgraph profiling

- important option: -fomit-frame-pointer

- perf has nice interface ('a' = "annotate") for reading assembly (good display of branches/jumps)

- A: optimized to no-op

- how to turn off optimizer

- profilers aren't infallible. a lot of the time samples are misattributed to neighboring ops

- fast mod example

- branch prediction hints (#define UNLIKELY(x), __builtin_expected, etc)

8 days ago by nhaliday

The Future of Mathematics? [video] | Hacker News

8 days ago 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 he end)

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 he end)

8 days ago by nhaliday

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

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

10 weeks ago by nhaliday

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

10 weeks ago by nhaliday

One week of bugs

may 2019 by nhaliday

If I had to guess, I'd say I probably work around hundreds of bugs in an average week, and thousands in a bad week. It's not unusual for me to run into a hundred new bugs in a single week. But I often get skepticism when I mention that I run into multiple new (to me) bugs per day, and that this is inevitable if we don't change how we write tests. Well, here's a log of one week of bugs, limited to bugs that were new to me that week. After a brief description of the bugs, I'll talk about what we can do to improve the situation. The obvious answer to spend more effort on testing, but everyone already knows we should do that and no one does it. That doesn't mean it's hopeless, though.

...

Here's where I'm supposed to write an appeal to take testing more seriously and put real effort into it. But we all know that's not going to work. It would take 90k LOC of tests to get Julia to be as well tested as a poorly tested prototype (falsely assuming linear complexity in size). That's two person-years of work, not even including time to debug and fix bugs (which probably brings it closer to four of five years). Who's going to do that? No one. Writing tests is like writing documentation. Everyone already knows you should do it. Telling people they should do it adds zero information1.

Given that people aren't going to put any effort into testing, what's the best way to do it?

Property-based testing. Generative testing. Random testing. Concolic Testing (which was done long before the term was coined). Static analysis. Fuzzing. Statistical bug finding. There are lots of options. Some of them are actually the same thing because the terminology we use is inconsistent and buggy. I'm going to arbitrarily pick one to talk about, but they're all worth looking into.

...

There are a lot of great resources out there, but if you're just getting started, I found this description of types of fuzzers to be one of those most helpful (and simplest) things I've read.

John Regehr has a udacity course on software testing. I haven't worked through it yet (Pablo Torres just pointed to it), but given the quality of Dr. Regehr's writing, I expect the course to be good.

For more on my perspective on testing, there's this.

Everything's broken and nobody's upset: https://www.hanselman.com/blog/EverythingsBrokenAndNobodysUpset.aspx

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

https://hypothesis.works/articles/the-purpose-of-hypothesis/

From the perspective of a user, the purpose of Hypothesis is to make it easier for you to write better tests.

From my perspective as the primary author, that is of course also a purpose of Hypothesis. I write a lot of code, it needs testing, and the idea of trying to do that without Hypothesis has become nearly unthinkable.

But, on a large scale, the true purpose of Hypothesis is to drag the world kicking and screaming into a new and terrifying age of high quality software.

Software is everywhere. We have built a civilization on it, and it’s only getting more prevalent as more services move online and embedded and “internet of things” devices become cheaper and more common.

Software is also terrible. It’s buggy, it’s insecure, and it’s rarely well thought out.

This combination is clearly a recipe for disaster.

The state of software testing is even worse. It’s uncontroversial at this point that you should be testing your code, but it’s a rare codebase whose authors could honestly claim that they feel its testing is sufficient.

Much of the problem here is that it’s too hard to write good tests. Tests take up a vast quantity of development time, but they mostly just laboriously encode exactly the same assumptions and fallacies that the authors had when they wrote the code, so they miss exactly the same bugs that you missed when they wrote the code.

Preventing the Collapse of Civilization [video]: https://news.ycombinator.com/item?id=19945452

- Jonathan Blow

NB: DevGAMM is a game industry conference

- loss of technological knowledge (Antikythera mechanism, aqueducts, etc.)

- hardware driving most gains, not software

- software's actually less robust, often poorly designed and overengineered these days

- *list of bugs he's encountered recently*:

https://youtu.be/pW-SOdj4Kkk?t=1387

- knowledge of trivia becomes more than general, deep knowledge

- does at least acknowledge value of DRY, reusing code, abstraction saving dev time

techtariat
dan-luu
tech
software
error
list
debugging
linux
github
robust
checking
oss
troll
lol
aphorism
webapp
email
google
facebook
games
julia
pls
compilers
communication
mooc
browser
rust
programming
engineering
random
jargon
formal-methods
expert-experience
prof
c(pp)
course
correctness
hn
commentary
video
presentation
carmack
pragmatic
contrarianism
pessimism
sv
unix
rhetoric
critique
worrydream
hardware
performance
trends
multiplicative
roots
impact
comparison
history
iron-age
the-classics
mediterranean
conquest-empire
gibbon
technology
the-world-is-just-atoms
flux-stasis
increase-decrease
graphics
hmm
idk
systems
os
abstraction
intricacy
worse-is-better/the-right-thing
build-packaging
microsoft
osx
apple
reflection
assembly
things
knowledge
detail-architecture
thick-thin
trivia
info-dynamics
caching
frameworks
generalization
systematic-ad-hoc
universalism-particularism
analytical-holistic
structure
tainter
libraries
tradeoffs
prepping
threat-modeling
network-structure
writing
risk
local-glob
...

Here's where I'm supposed to write an appeal to take testing more seriously and put real effort into it. But we all know that's not going to work. It would take 90k LOC of tests to get Julia to be as well tested as a poorly tested prototype (falsely assuming linear complexity in size). That's two person-years of work, not even including time to debug and fix bugs (which probably brings it closer to four of five years). Who's going to do that? No one. Writing tests is like writing documentation. Everyone already knows you should do it. Telling people they should do it adds zero information1.

Given that people aren't going to put any effort into testing, what's the best way to do it?

Property-based testing. Generative testing. Random testing. Concolic Testing (which was done long before the term was coined). Static analysis. Fuzzing. Statistical bug finding. There are lots of options. Some of them are actually the same thing because the terminology we use is inconsistent and buggy. I'm going to arbitrarily pick one to talk about, but they're all worth looking into.

...

There are a lot of great resources out there, but if you're just getting started, I found this description of types of fuzzers to be one of those most helpful (and simplest) things I've read.

John Regehr has a udacity course on software testing. I haven't worked through it yet (Pablo Torres just pointed to it), but given the quality of Dr. Regehr's writing, I expect the course to be good.

For more on my perspective on testing, there's this.

Everything's broken and nobody's upset: https://www.hanselman.com/blog/EverythingsBrokenAndNobodysUpset.aspx

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

https://hypothesis.works/articles/the-purpose-of-hypothesis/

From the perspective of a user, the purpose of Hypothesis is to make it easier for you to write better tests.

From my perspective as the primary author, that is of course also a purpose of Hypothesis. I write a lot of code, it needs testing, and the idea of trying to do that without Hypothesis has become nearly unthinkable.

But, on a large scale, the true purpose of Hypothesis is to drag the world kicking and screaming into a new and terrifying age of high quality software.

Software is everywhere. We have built a civilization on it, and it’s only getting more prevalent as more services move online and embedded and “internet of things” devices become cheaper and more common.

Software is also terrible. It’s buggy, it’s insecure, and it’s rarely well thought out.

This combination is clearly a recipe for disaster.

The state of software testing is even worse. It’s uncontroversial at this point that you should be testing your code, but it’s a rare codebase whose authors could honestly claim that they feel its testing is sufficient.

Much of the problem here is that it’s too hard to write good tests. Tests take up a vast quantity of development time, but they mostly just laboriously encode exactly the same assumptions and fallacies that the authors had when they wrote the code, so they miss exactly the same bugs that you missed when they wrote the code.

Preventing the Collapse of Civilization [video]: https://news.ycombinator.com/item?id=19945452

- Jonathan Blow

NB: DevGAMM is a game industry conference

- loss of technological knowledge (Antikythera mechanism, aqueducts, etc.)

- hardware driving most gains, not software

- software's actually less robust, often poorly designed and overengineered these days

- *list of bugs he's encountered recently*:

https://youtu.be/pW-SOdj4Kkk?t=1387

- knowledge of trivia becomes more than general, deep knowledge

- does at least acknowledge value of DRY, reusing code, abstraction saving dev time

may 2019 by nhaliday

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

november 2016 by nhaliday

local vs. global errors in technical papers

old:

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

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

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

november 2016 by nhaliday

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

november 2016 by nhaliday

compilation errors in academic papers

old:

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

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

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

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

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

november 2016 by nhaliday

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

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

july 2016 by nhaliday

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

july 2016 by nhaliday

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

june 2016 by nhaliday

Terry Tao:

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

fedja:

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

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

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

Timothy Chow:

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

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

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

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

fedja:

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

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

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

Timothy Chow:

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

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

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

june 2016 by nhaliday

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

may 2016 by nhaliday

thinking like a mathematician

some of the points:

- small # of tricks (echoes Rota)

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

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

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

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

- small # of tricks (echoes Rota)

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

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

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

may 2016 by nhaliday

On writing | What's new

april 2016 by nhaliday

also: on reading papers

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

Work hard | What's new

april 2016 by nhaliday

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

- from the comments

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

april 2016 by nhaliday

Lean

january 2016 by nhaliday

https://lean-forward.github.io

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

mostly happening in the Netherlands

https://formalabstracts.github.io

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

- Thomas Hales

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

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.

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

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

mostly happening in the Netherlands

https://formalabstracts.github.io

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

- Thomas Hales

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

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.

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

january 2016 by nhaliday

**related tags**

Copy this bookmark: