Schlagwort: Mathematik

Proof Standards.

Any artificially generated mathematical text will not be considered as a proof unless:
- It has been communicated in both a natural language text paired with a computer formalization of all definitions, theorems, and proofs.
- The formalization has been accepted by the proof assistant and human expert referees have vetted both the formalization and the paired text.

Emily Riehl: A New Paradigm for Mathematical Proof?

Slop Slogging.

We are in fact faced with a challenge to devise methods of buying originality with plodding, now that we are in possession of slaves which are such persistent plodders.

Hao Wang: Toward mechanical mathematics (1960)

No lonely group.

Group membership limit must be greater than 1.

Canvas LMS

Real and complex.

I was a twenty-seven-year-old college dropout before I finally met some real mathematicians and found that those people don’t even give a shit about calculus.

Neal Stephenson: Termination Shock

Future Prophecies.

  • an intuitive and feature rich theorem prover language. one that both mathematicians with an interest in programming and programmers with an interest in maths can start to use without too much hassle. in 2122 you won't graduate from your maths degree without knowing how to prove theorems with a computer.
  • intuitive and feature rich formal verification frameworks for the major programming languages. in 2122, ADA SPARK will not be your only option for critical software.
  • extensive use and major discoveries regarding homomorphic encryption. many services will be required by law to only process data in this manner. in 2122 fully E2E encrypted applications will offer a wide degree of functionalities that is currently only possible through services which can read you data in the clear.

fickle nest: 3 things for the next 100 years of Computer Science