VR interface / college project

Stream: new members

[Landry Morel]

Hello world !
My name is Landry Morel, I am a graduate student at UC-Berkeley and a former maths major at Paris V Descartes. I currently have a project for one of my classes where I have to build a VR game. I have always wanted to create a new medium for doing maths, and handling concepts through gesture and a Man-Machine-Interface rather than chalk and talk really feels like a promising idea. I humbly come to the Lean community for guidance, as I might not be the first with this dream. I am specifically reaching out to teachers/enthusiasts that have tried the current VR offerings for math lessons to give me a baseline understanding of the state of VR maths classrooms.
Thank you !

[Kevin Buzzard]

What does VR mean? You mean headsets? What does this have to do with lean?

[Landry Morel]

I do mean Virtual Reality, with headsets and joysticks. I believe that Lean has a tactics structure that could be built upon (or even power entirely) the game I am trying to build
The endgame is to provide for high-schoolers/college undergraduates with a very intuitive way to engage with their classes while keeping the rigor and methodology needed for academia

[Patrick Johnson]

Whatever you're planning to implement, I wish you a great luck. And please make it open-source.

[Arthur Paulino]

Reminded me of this:
Arthur Paulino said:

Am I too crazy to dream about a future in which humans will be doing mathematics with some ultra high tech interface that projects things in 3D and people will find and understand results by literally dragging and dropping pieces of a puzzle?

In my imagination, there are some amazing possibilities that open up with this kind of hardware.
One is being able to see multiple goal states floating in my eye sight, each of them being the result of the application of certain tactics to help me choose how I want to proceed. And with a flick of a hand, it would show me lemmas/theorems that are similar to the current result I have to prove

[Landry Morel]

Patrick Johnson said:

Whatever you're planning to implement, I wish you a great luck. And please make it open-source.

Thank you !
I am more inclined than not to make it open-source, if it ends up being usable and not just a tech demo

[Landry Morel]

Arthur Paulino said:

Reminded me of this:
Arthur Paulino said:

Am I too crazy to dream about a future in which humans will be doing mathematics with some ultra high tech interface that projects things in 3D and people will find and understand results by literally dragging and dropping pieces of a puzzle?

In my imagination, there are some amazing possibilities that open up with this kind of hardware.
One is being able to see multiple goal states floating in my eye sight, each of them being the result of the application of certain tactics to help me choose how I want to proceed. And with a flick of a hand, it would show me lemmas/theorems that are similar to the current result I have to prove

Yes this is exactly the goal ! Even if it might not be trivial to find ways to represent the most advanced mathematical constructs, I am fairly certain that most of undergrad arithmetic, pre-hilbertian algebra, real/complex analysis and probabilities/statistics could greatly benefit from a gamey interface.