Games

Digital

• QED
• Emojic
• Nand Game
• Natural Deduction
• Pebble Games
• Economics Games
• FindX
• Algebra Game
• Axolot
• Natural Numbers Game
• Cassandra Xia's Games

Physical

• Hard Choices
• Zendo
• Black Box
• Set
• Color Code
• Entropy
• https://en.wikipedia.org/wiki/List_of_abstract_strategy_games#Other_games

Interactives

• Digital Mathematics
• Learning Machines
• https://lewiscarrollresources.net/gameoflogic/index.html
• https://votbear.itch.io/oddeasy

Tools

• Gambit
• Group Explorer
• Combinatorial Game Suite
• Collaborative Calculation and Data Science
• CalcCheck
• Proof Designer
• Lurch
• Apros
• WebWork
• DeltaMath
• Geometer's Skechpad
• Lambda Reducer
• Lambda Calculator
• Elfe
• Logitext
• Sequent Calculus Trainer
• SAD
• Aprove
• ProofToys
• CoqGym
• MathEdit
• ProvingGround
• Tutch
  • Demo
• Ollibot
• Pandora
• Fitch
• Teaching Logic
• Conan
• http://www.conceptuamath.com/math-tools/
• http://proofs.openlogicproject.org/
• https://www.gradegrinder.net/index.html

Products

• Edukera
• Brilliant
• Brain HQ
• Cognifit
• Imandra
• 4Ferries

Organizations

• Imaginary
• Experimental Geometry Lab
• NeuroScape
• VeconLab - sadz 2011
• Theorem proving components for Educational software
• Naproche
• FMathL
• LeoII
• Digital Grammars
• MathCat
• Evidence Algorithm
• ISAAC
• ISAC
• RISC
• MathToys
• Collab
• Xena Project
• Proving for Fun
• Big Proof
• xAPI
• YouCubed
• POEM Lab
• Verimag

Courses

• Constructive Logic Software

Blogs

• I speak math
• https://andymatuschak.org/
• http://www.scottfarrar.com/sfx/
• http://worrydream.com/Links2013/
• https://numinous.productions/ttft/

Texts

General

• Connecting Abstract Algebra to Secondary Mathematics, for Secondary Mathematics Teachers
• The Language of Mathematics: A Linguistic and Philosophical Investigation
• Proof Technology in Mathematics Research and Teaching

Sage

• http://abstract.ups.edu/aata/aata.html
• http://linear.pugetsound.edu/html/fcla.html

R

• https://cran.r-project.org/web/packages/matlib/
• https://otexts.org/fpp2/
• https://www.datacamp.com/courses/forecasting-using-r
• https://www.datacamp.com/courses/linear-algebra-for-data-science-in-r

Lean

• Logic and Proof

ISETL

• Learning Abstract Algebra with ISETL

Inquiry

• Linear Algebra
• Diff Eq
• Groups

Reading -- need to organize

• Teaching calculation and discrimination: a more effective curriculum
• Algebriac Games
• The Effects of Modern Mathematics Computer Games on Mathematics Achievement and Class Motivation
• An Abstract Algebra Story
• Implementing inquiry-oriented curriculum: From the mathematicians’ perspective
• Developing instructor support materials for an inquiry-oriented curriculum
• Insights and Recommendations from theMAA National Study of College Calculus
• Teaching and Learning Group Theory
• The Effects of Mathematical Game Play on the Cognitive and Affective Development of Pre-Secondary Students
• Designing and Testing a Mathematics Card Game for Teaching and Learning Elementary Group Theory
• Exploring an Instructional Model for Designing Modules for Secondary Mathematics Teachers in an Abstract Algebra Course
• Computer games application within alternative classroom goal structures: cognitive, metacognitive, and affective evaluation
• The effects of modern mathematics computer games on mathematics achievement and class motivation.
• Learning middle school mathematics through student designed and constructed video games
• Mobile Math
• Beyond edutainment: Exploring the educational potential of computer games
• Games, learning & society: Centers of expertise for academic learning through open-ended video games
• Collaborative learning, reasoning, and technology
• Developing realistic mathematics education
• Revisiting mathematics education. China Lectures
• Group Theory, Game Theory, a bit of Philosophy and a post in Tao's blog
• GAMIFICATION OF AN UNDERGRADUATE PSYCHOLOGY STATISTICS LAB: BENEFITS TO PERCEIVED COMPETENCE15
• Game Theory and interactive learning
• Strategies for Computer-Based Programming Instruction: Program Completion vs. Program Generation
• A Theorem Prover for Scientific and Educational Purposes
• Theorem Provers as a Learning Tool in Theory of Computation
• Learning how to Prove: From the Coq Proof Assistant to Textbook Style
• The Sequent Calculus Trainer with Automated Reasoning - Helping Students to Find Proofs
• Pandora: A Reasoning Toolbox using Natural Deduction Style.
• Ten years of computer-based tutors for teaching logic 2000-2010: Lessons learned
• A teaching tool for proving equivalences between logical formulae
• A web-based interactive system for learning FOL to CF conversion
• AXolotl: A Self-study Tool for First-order Logic
• A Mobile Application for Self-Guided Study of Formal Reasoning
• Introduction to Iltis: an interactive, web-based system for teaching logic
• Automated Scaffolding and Feedback for Proof Construction: A Case Study
• Towards Intuitive Reasoning in Axiomatic Geometry
• The Elfe System - Verifying mathematical proofs of undergraduate students
• Desirable features of educational theorem provers
• Evaluating the Usability of Interactive Verification Systems.
• An empirical evaluation of two user interfaces of an interactive program verifier
• How to put usability into focus: using focus groups to evaluate the usability of interactive theorem provers
• Theoretical models of the role of visualisation in learning formal reasoning
• Towards Usability Evaluation of Interactive Theorem Provers
• Re-purposing Google maps visualisation for teaching logistics systems
• A usability evaluation of interactive theorem provers using focus groups
• An Interaction Concept for Program Verification Systems with Explicit Proof Object
• An empirical evaluation of two user interfaces of an interactive program verifier
• Interactive Theorem Proving-Modelling the User in the Proof Process.
• The KeYmaera X Proof IDE
• Evidential Paradigm and SAD Systems: Features and Peculiarities
• ELFE – An interactive theorem prover for undergraduate students
• The Higher-Order Prover Leo-II
• Proof-checking mathematical texts in controlled natural language
• Developing the System MathNat for Automatic Formalization of Mathematical texts
• A Fully Automatic Theorem Prover with Human-Style Output
• A language for mathematical knowledge management
• The Need for Proof and Proving: Mathematical and Pedagogical Perspectives
• Teaching the Formalization of Mathematical Theories and Algorithms via the Automatic Checking of Finite Models
• Prototyping “Systems that Explain Themselves” for Education
• The math problem inside every math problem
• Automated Generation of User Guidance by Combining Computation and Deduction

Models

• Toward a modeling theory of physics instruction
• Visualisation and Cognition: Drawing Things Together

Back and forth games

• Entropy and Matrix Multiplication Games

Applications

• FORMAL ABSTRACTION IN ENGINEERING EDUCATION — CHALLENGES AND TECHNOLOGY SUPPORT
• FACHLICHES PROBLEMLÖSEN IN DER MASCHINENKONSTRUKTION - UNTERSUCHUNG VON STRUKTUR UND ERLERNBARKEIT MITTELS MULTIMODALER TECHNIKMODELLE
• Technologies for Models of Mathematics

ML

• Learning to Prove Theorems via Interacting with Proof Assistants

Inteligent Tutoring Systems

• Wikipedia
• Improving QED-Tutrix by Automating the Generation of Proofs
• QED-TUTRIX : SYSTÈME TUTORIEL INTELLIGENT POUR L'ACCOMPAGNEMENT DES ÉLÈVES EN SITUATION DE RÉSOLUTION DE PROBLÈMES DE DÉMONSTRATION EN GÉOMÉTRIE PLANE
• GeoGebraTUTOR : Développement d’un système tutoriel autonome pour l’accompagnement d’élèves en situation de résolution de problèmes de démonstration en géométrie plane et genèse d’un espace de travail géométrique idoine

Theorem Proving

• Q0
• Formula editors for tp-based systems. state of the art and prototype implementation in ISAC

Logics

• Human-Readable Machine-Verifiable Proofs for Teaching Constructive Logic
• Friendly e-tutor for Natural Deduction
• Pandora: A Reasoning Toolbox using Natural Deduction Style
• The Evaluation of an Educational Aiding Tool for Students Learning Logic
• Proof Editor for Natural Deduction in First-order Logic The Evaluation of an Educational Aiding Tool for Students Learning Logic

Proof

• Structured Derivations: a Unified Proof Style for Teaching Mathematics

Ehrenfeucht-Fraisse Games

• Descriptive Complexity: Ehrenfeucht-Fraisse Games

Game Theory

• Backward Induction
• Checkmate: Exploring backward induction among chess players
• Stochastic game theory: For playing games, not just for doing theory
• Game Theory through Examples
• Restoring Fun to Game Theory
• Epiphany in the Game of 21
• Active Learning with Monty Hall in a Game Theory Class
• Epistemic Game Theory: Putting Algorithms to Work
• I Think You Think I Think You're Lying: The Interactive Epistemology of Trust in Social Networks
• Linking GameTheoretical Approaches with Constructive Type Theory
• First steps in constructive game theory

DragonBox

• The Effects of Mathematical Game Play on the Cognitive and Affective Development of Pre-Secondary Students
• THE INFLUENCE OF DRAGONBOX ON STUDENT ATTITUDES AND UNDERSTANDING IN 7TH GRADE MATHEMATICS CLASSROOM
• THE EFFECT OF USING DRAGONBOX ON THE MATHEMATICS TEACHING EFFICACY OF PRESERVICE MIDDLE GRADE TEACHER

Learning Analytics and Educational Data Mining

• Educational Data Mining
• User Modeling
• International Society of Learning Science
• Penetrating the fog: Analytics in learning and education
• Translating learning into numbers: A generic framework for learning analytics
• A reference model for learning analytics
• Let's not forget: Learning analytics are about learning
• Learning analytics and educational data mining: towards communication and collaboration
• Creating Effective Learning Analytics Dashboards: Lessons Learnt
• Measuring actual learning versus feeling of learning in response to being actively engaged in the classroom

Gamification

• Challenge Based Learning: The Report from the Implementation Project
• Does gamification work? a literature review of empirical studies on gamification
• How to use Gamified Dashboards and Learning Analytics for Providing Immediate Student Feedback and Performance Tracking in Higher Education
• Integration of Learning Analytics techniques and Gamification: an experimental study
• From game design elements to gamefulness: Defining “gamification.”
• Uses and Gratifcations of Initiating Use of Gamifed Learning Platforms
• Validating the Effectiveness of Data-Driven Gamification Recommendations: An Exploratory Study
• Analysing gamification elements in educational environments using an existing Gamification taxonomy
• Gamifying education: what is known, what is believed and what remains uncertain: a critical review
• A Critique and Defense of Gamification
• Leveraging on Gamification and Learning Analytics for Improved Student Learning
• Investigating Gamification and Learning Analytics Tools for Promoting and Measuring Communities of Inquiry in Moodle Courses
• Gamification and Learning Analytics to Improve Engagement in University Courses

Probability and Statistics

It's unclear how to relate this to any game / proof techniques.

• Constructing a logic of plausible inference: a guide to Cox’s theorem
• Fundamentals of statistical causality
• Rubin Causal Model
• The Neyman-Rubin Model of Causal Inference and Estimation via Matching Methods
• Causal Inference for Statistics, Social, and Biomedical Sciences: An Introduction
• Probability Box
• Developing Interactive Tools for Teaching Statistics to Psychology Students
• Teaching Research Methods and Statistics in eLearning Environments: Pedagogy, Practical Examples, and Possible Futures
• Seeing Theory
• GeoGebra in Teaching and Learning Introductory Statistics
• ISLP
• Alex Reinhart Pedagogy
• Teaching Statistics Group

AI and Machine Learning

• OkAI

Data Science

• Ohmage
• Concord
• Pisa
• 50 years of statistics teaching in English schools: some milestones
• K-12 Data Literacy
• Introduction to Data Science
• ISLE

Game Design

• https://en.wikipedia.org/wiki/Game_mechanics
• Formal Models and Game Design
• DISCO, a Formal Model of Serious Games to Help Teachers at the Design Stage
• Interdisciplinary Models and Tools for Serious Games
• Exploring Games as Formal Models
• Deriving Quests from Open World Mechanics
• The Design of Artifacts for Augmenting Intellect

Mental IMagery

• https://www.frontiersin.org/articles/10.3389/fpsyg.2019.02034/full

Related Work

Music

• LightNote
• Teoria
• uTheory
• Hookpad
• Notation Training
• Syntorial
• Learning Synths
• Toned Ear
• Yousician

Algorithms

• https://www.redblobgames.com/pathfinding/a-star/introduction.html
• https://www.csunplugged.org/en/
• https://blog.acolyer.org/2019/04/17/teaching-rigorous-distributed-systems-with-efficient-model-checking/
• https://runway.systems/
• http://www.r2d3.us/visual-intro-to-machine-learning-part-1/
• http://setosa.io/ev/

Physics

• https://twitter.com/InertialObservr/status/1153018532369555456
• https://quantum.country/
• https://mitpress.mit.edu/sites/default/files/titles/content/sicm_edition_2/book.html

Econ

• https://github.com/norvig/pytudes/blob/master/ipynb/Economics.ipynb
• https://play.beatsempire.org/
• http://titan.ja.org/
• https://robosellers.ja.org/

Software

• https://react-devtools-tutorial.now.sh/
• https://illustrated.dev/

Maths

• https://early.khanacademy.org/
• https://explorabl.es/math/
• https://littlegrayfieldhouse.itch.io/

Computational THinking

• https://www.wolfram.com/programming-lab/
• http://www.wolfram.com/language/elementary-introduction/
• http://education.wolfram.com/summer/
• https://csunplugged.org/en/
• https://docs.google.com/document/d/1r1b2CM1uTdST47IbWa7zlZYmbfoqrgYSeym2inUvnFo/edit

Prototypes

Experiments Game

• https://probcomp.github.io/Gen/
• Trace Types and Denotational Semantics for Sound Programmable Inference in Probabilistic Languages
• http://probcomp.csail.mit.edu/software/bayesdb/
• http://probcomp.csail.mit.edu/software/open-probabilistic-programming-stack/
• Introduction to probasbilistic programmying
• Foundations of Constructive Probability Theory
• The definition of random sequences - Per martin lof - universal test of randomness
• A shiny update to an old experiment game
• Statistical Games as Teaching Aids
• An experiement game
• Using the board game Borel to illustrate probability calculation
• Assemble to Order Simulator

QED with a better UI

Logic Game Engine

• http://projects.illc.uva.nl/GLoRiClass/
• http://www.logicinaction.org/docs/ch7.pdf
• Saying It with Pictures: a logical landscape of conceptual graphs
• Playing Lorenzen Dialogue Games on the Web∗
• Interpreting Sequent Calculi as Client-Server Games
• Dialogues for proof search

Probability Distribution Game

• https://nskobelevs.github.io/p5js/BayesTheorem/

QED with a better UI

Logic Game Engine

• http://projects.illc.uva.nl/GLoRiClass/
• http://www.logicinaction.org/docs/ch7.pdf
• Saying It with Pictures: a logical landscape of conceptual graphs
• Playing Lorenzen Dialogue Games on the Web∗
• Interpreting Sequent Calculi as Client-Server Games
• An Automated Method for Building Cognitive Models for Turn-Based Games from a Strategy Logic
• [Bridging the gap between logic and cognition: a translation method for centipede games(http://fse.studenttheses.ub.rug.nl/15845/1/hmc_thesis_s2402319.pdf)

Carnap Extension

• The Proof Complexity of Linear Algebra

Diagrammatic Reasoning

• http://homepages.math.uic.edu/~kauffman/Laws.pdf
• https://graphicallinearalgebra.net/
• https://suhr.github.io/papers/calg.html
• http://jlazovskis.com/docs/PenTen.pdf
• https://github.com/fluorine/GraphicMathNotation
• https://www.ioc.ee/~pawel/
• http://homepages.math.uic.edu/~kauffman/Form.html
• http://www.crissp.be/wp-content/uploads/2018/02/jasperssmessaert.pdf
• The Emergence of Orientation and the Geometry of Logic
• http://www.markability.net/prospectus.htm
• Diagrammatic logic and game-playing
• EXISTENTIAL GRAPHS AS AN INSTRUMENT OF LOGICAL ANALYSIS
• Existential Graphs as a basis for structured reasoning
• A diagrammatic formal system for euclidean geometry

Orders

• http://www.rntz.net/files/tones.pdf

Linear equation manipulator

Aproximation?

Trig

• http://chalkdustmagazine.com/blog/how-to-calculators-do-trigonometry/

Alg

• http://chalkdustmagazine.com/features/on-sqrt-2/
• https://en.wikipedia.org/wiki/Chakravala_method

Equational Logic

• http://www.cs.cornell.edu/home/gries/Logic/Equational.html