Implementing mathematical theorems

Question

This is a general design question on implementing math theorems. I am trying to implement some math theorems, from differential geometry, in a programming language (it doesn't matter which; for simplicity I use the python language, but this should not affect the general ideas.). I can describe the question better with an example.

Theorem: Any straight line on a surface of class r>= 2 is an asymptotic curve.

How would be such a theorem implemented. Obviously the function needs a line as an argument and the surface as an argument.

def theorem (line, surface): pass

Should the function return just true, false, or undecidable? Or should the function return "asymptotic". If we name the function "is-asymptotic", then it should return true, false, or undecidable.

The first thing that the function should check is if the line is straight. Let's don't go into details. Then, it should compute the class of the surface

def theorem (line, surface): 
  if not straight(line, surface):
    return "undecidable"
  else:
    if class-of(surface) >= 2:
      ???

The above approach drives me to return true/false. On the other hand, if I implement it as a method to a class called line, that asks for all the properties of the given line then it should return a list of properties, including "asymptotic".

Finally, what I did above is to ask for a property of a given line, our argument. The function says nothing about all the other straight lines.

How would you address the whole implementation design of theorems?

Thank you in advance.

PS. In order to further clarify the question in a programming language content, the above question is rephrased as following. Assuming I have an instance "line" of the object "Line". Do I ask the instance if it is asymptotic as in

is_asymptotic(line) # returns true/false/undecidable

or do I ask for its properties and get a list of properties which includes the asymptotic property, as in

line_properties(line) # returns [..., "asymptotic", ...]

or on the creation of the instance I set the attribute asymptotic, after checking if it is straight, as in

line = Line(surface) # sets line.asymptotic = True

Answer 1

use the sympy package.

In [153]: from sympy import *
In [154]: x = symbols('x')
In [155]: y = symbols('y')
In [156]: z = symbols('z')
In [157]: p = (x+y)**2
In [158]: p
Out[158]: (x + y)**2
In [159]: q = x**2 + 2*x*y + y**2
In [160]: p == q
Out[160]: False
In [161]: p.expand() == q
Out[161]: True

you will likely find https://github.com/sympy/sympy/wiki/Geometry-Module

to be helpful.

good luck!