Skip to main content
SixWingedSeraph's user avatar
SixWingedSeraph's user avatar
SixWingedSeraph's user avatar
SixWingedSeraph
  • Member for 15 years, 2 months
  • Last seen more than 7 years ago
awarded
awarded
awarded
awarded
awarded
awarded
comment
Uniqueness Principle for function types
This question shows a common problem that many students have with definitions in math. It comes up when you define a word that already has connotations, in this case "function". The only data you can use in proofs based on this new definition are the properties given by the definition (until someone has proved some theorems you can use). If the fact that a function in the general usage of mathematical English is determined by its values is not given in the definition, you can't use it. In general, if you see a math definition of a word, throw away its connotations!
awarded
comment
What technical and/or theoretical challenges are involved in automatically extracting proofs from books and papers into Coq code?
The problems in understanding mathematical English, even in formally written papers, is well described in the book The Language of mathe­matics, by Mohan Ganesalingam, and many other examples are given in my website athttp://www.abstractmath.org/MM/MMLangMath.htm
awarded
awarded
Loading…
awarded
awarded
awarded
awarded
awarded
awarded
awarded