'It Feels Like Sort of Cheating in Some Ways That You Don't Fully Show That You've Understood the Proofs': Mathematics Students Coding Proofs with an Interactive Theorem Prover

Artigo2026

0 visualizações desta ficha 0 acessos ao texto completo Contagem real do Portal desde 25/09/2026; tráfego comum, sem testes; quem desativa o rastreamento no navegador não é contado.

Texto completo não localizado nas fontes consultadas. O registro é mantido pela pertinência.

Resumo

Interactive theorem provers such as Lean are increasingly used in mathematics research and are now introduced into university mathematics teaching. One widely used resource for the introduction to Lean, one such interactive theorem prover, is the Natural Number Game. This gamified learning environment introduces formal proof writing in Lean through interactive exercises (levels) based on statements about natural numbers. However, little is known about undergraduate students' proof activity in this environment and its key characteristics. In this paper, we adopt the instrumental approach to analyse video-recorded, task-based interviews with two undergraduate mathematics students as they go through the Natural Number Game. This approach allows us to characterise two distinct ways of interacting with the tool, illustrating contrasting perspectives and approaches which may support learning mathematics in different ways. Our findings have implications for students' use of interactive theorem provers as part of mathematics learning at university and the understanding of mathematical proof.

Dados da obra

Tipo: Artigo
Periódico: Digital Experiences in Mathematics Education
Ano: 2026
Idioma: en
Palavras-chave: Mathematics Instruction; Gamification; Undergraduate Students; Mathematical Logic; Validity; College Mathematics; Student Attitudes
ISSN: 2199-3246
Acesso: Metadados apenas
Fontes: ERIC — Education Resources Information Center
Na Biblioteca desde: 01/10/2026 · verificada em 03/10/2026

Como citar

ABNT
IANNONE, Paola; THOMA, Athina. 'It Feels Like Sort of Cheating in Some Ways That You Don't Fully Show That You've Understood the Proofs': Mathematics Students Coding Proofs with an Interactive Theorem Prover. Digital Experiences in Mathematics Education, 2026. Disponível em: http://dx.doi.org/10.1007/s40751-025-00193-w. Acesso em: 5 nov. 2026.

APA

Iannone, P., & Thoma, A. (2026). 'It Feels Like Sort of Cheating in Some Ways That You Don't Fully Show That You've Understood the Proofs': Mathematics Students Coding Proofs with an Interactive Theorem Prover. Digital Experiences in Mathematics Education. http://dx.doi.org/10.1007/s40751-025-00193-w

BibTeX

@article{iannone2026,
  author = {Iannone, Paola and Thoma, Athina},
  title = {'It Feels Like Sort of Cheating in Some Ways That You Don't Fully Show That You've Understood the Proofs': Mathematics Students Coding Proofs with an Interactive Theorem Prover},
  year = {2026},
  journal = {Digital Experiences in Mathematics Education},
  url = {http://dx.doi.org/10.1007/s40751-025-00193-w},
  language = {en}
}

RIS

TY  - JOUR
AU  - Iannone, Paola
AU  - Thoma, Athina
TI  - 'It Feels Like Sort of Cheating in Some Ways That You Don't Fully Show That You've Understood the Proofs': Mathematics Students Coding Proofs with an Interactive Theorem Prover
PY  - 2026
JO  - Digital Experiences in Mathematics Education
UR  - http://dx.doi.org/10.1007/s40751-025-00193-w
LA  - en
ER  -

Referência gerada automaticamente a partir dos metadados das fontes; confira com o documento original. Baixar BibTeX · Baixar RIS