An Idea for an Online Proof Game

[middleCmusic]

Hey everyone,

I'll start this off by saying that I am no computer programmer and only a junior undergrad studying math.

But, I have an idea for a math-based game that I think would be really awesome to train students in the art of proving/problem solving. It is the following:

The goal of each game is to prove a given theorem. You are given the results and the implications in two inventory boxes which you can drag into the main workflow to connect statements together. For example, say that you were proving that √2 is irrational.

In the implications box (made up of previously proved theorems,definitions, and axioms) you might have the following [in a random order]:

* For any rational number q, q = a/b where a and b are both integers
* When both sides of an equation are multiplied by the same quantity, the resulting equation is true
* When both sides of an equation are squared, the resulting equation is true
* We may reduce any rational number so that its numerator and denominator share no common factors.
* n is even if and only if n = 2k for some integer k.
* When a quantity equal to a given quantity is substituted into the equation, the resulting equation is true
* Cancellation law for the rational numbers
* If an assumption is made and the negation of that assumption is shown to be true, the assumption was false.

Then in the results box, you would have [again, in a random order]:

* √2 is rational
* √2 = a/b for a, b integers
* √2 = p/q for p, q integers with no common factors
* q√2 = p
* 2q^2 = p^2
* p^2 is even
* p is even
* p = 2k for some integer k
* 2q^2 = 4k^2
* q^2 = 2k^2
* q^2 is even
* q is even
* p and q share a common factor
* √2 is irrational

Whenever you correctly connect two results with an implication, it would light up and you would get points. Also, if someone came up with better names than 'results' and 'implication', that would be cool too.

An easier version would be to put the results in the correct order and ask the player to simply connect them with the appropriate logical steps.

I think this game would be great for teaching college students, and even younger kids, about the principles of logic and proof techniques. I simply don't have the computer know-how to make anything like this happen.

Furthermore, one could hope in the future to combine all the results and implications in the game into a conjecture-proving crowd-sourced version, which would let people try and make the connections from one known statement to the proof of a conjecture. Obviously, each step in the proof to the conjecture would have to be in the game, but it doesn't seem so far-fetched to me that there could be some genuine progress from this game. Much like that game that allows people to manipulate proteins to solve chemical problems.

Anyone want to make this happen? I'm thinking you could call it "Prove It", if that's not already copyrighted.

 

[Robert1986]

Well, I'm not sure how I feel about this. Doing math is a lot about creativity. With this kind of game you are kind of forcing people to prove stuff in a certain way (or ways). Also, you kind of give away the proof - just in a jumbled order.

 

[middleCmusic]

Well, I'm not sure how I feel about this. Doing math is a lot about creativity. With this kind of game you are kind of forcing people to prove stuff in a certain way (or ways). Also, you kind of give away the proof - just in a jumbled order.

All good points. I'll say two things:

1) You're right that there are always many, if not infinite possible ways of doing a proof. However, most people, even math majors, do the pedagogical classics in practically the same way every time.

2) It's also true that this wouldn't be very hard for some people - but I think it would be helpful for a lot of people, especially for people for whom logic and proving doesn't come naturally. I also think that it would be harder if you've never seen the proof in question before and if it's out of order.

 

[chiro]

Hey middleCmusic.

You might want to consider some kind of directed graph that represents a proof through transitions of a particular statement where the starting node is the starting statement and the ending node is the ending statement.

What goes in between are the possibilities of entire proofs which make up one sequence from start to finish (and you can have as many things in between as you want).

You can then come up with algorithms to generate the graph structures using your mathematical domain knowledge.

 

[middleCmusic]

Hey middleCmusic.

You might want to consider some kind of directed graph that represents a proof through transitions of a particular statement where the starting node is the starting statement and the ending node is the ending statement.

What goes in between are the possibilities of entire proofs which make up one sequence from start to finish (and you can have as many things in between as you want).

You can then come up with algorithms to generate the graph structures using your mathematical domain knowledge.

Thanks for the input, chiro. Are you suggesting trying to create a game in which the user's proof techniques are recognized through some sort of logical processor? Or just one in which many different proofs are stored for any given topic. I know that there are some "proving" programs that attempt to prove things without human input through a logical calculus, but I don't know how effective they are and/or if they can recognize human reasoning and verify that it's valid. Is that what you were getting at?

 

[chiro]

Basically my suggestion is the following:

You have a proof represented in a graph structure that is acyclic and directed where each path is a potential way of proving something.

You come up with algorithms to generate the graph for a particular kind of proof (So as an example one for diophantine problems, one for calculus, and so on).

You then store these structures somewhere in memory or on hard drive.

Within the graph you add information about the transformation and present on screen for options the proofs start and final node.

Within the proof exercise you get metadata from the proof graph and build a program to recognize a users transformation with a node in the graph.

Once you have found a potential new node, you give the user a tick for the right transformation and then check the child nodes for a new possible transformation.

You keep repeating until you make a path from root node to final node in which the proof is completed by the user.

The main challenges will be constructing the proof graph and coming up with an intuitive system to resolve a valid transformation with an intuitive user based input scheme.