As new technological developments continue to change the educational landscape, it is not an exception in the area of proof and proving. This classroom note introduces the use of one of the trending proofs assistants -- the Lean theorem prover. We first provide a technical account of Lean, then exemplify Lean proofs in propositional logic, number…

Scale validation is vital to psychological research because it ensures that scores from measurement scales represent the intended construct. Factor analysis fit indices are commonly used to provide quantitative evidence that a proposed factor structure is plausible. However, there is mismatch between guidelines for evaluating fit of factor models…

Researchers often study dynamic processes of latent variables in everyday life, such as the interplay of positive and negative affect over time. An intuitive approach is to first estimate the measurement model of the latent variables, then compute factor scores, and finally use these factor scores as observed scores in vector autoregressive…

Bayesian Knowledge Tracing, a model used for cognitive mastery estimation, has been a hallmark of adaptive learning research and an integral component of deployed intelligent tutoring systems (ITS). In this paper, we provide a brief history of knowledge tracing model research and introduce pyBKT, an accessible and computationally efficient library…

Network meta-analysis has played an important role in evidence-based medicine for assessing the comparative effectiveness of multiple available treatments. The prediction interval has been one of the standard outputs in recent network meta-analysis as an effective measure that enables simultaneous assessment of uncertainties in treatment effects…

Purpose: This study investigates the impact of AI-assisted pair programming on undergraduate students' intrinsic motivation, programming anxiety, and performance, relative to both human-human pair programming and individual programming approaches. Methods: A quasi-experimental design was conducted over two academic years (2023-2024) with 234…

Programming is becoming increasingly common in mathematics degrees as it is a desirable skill for new graduates. However, research shows that its use is mostly restricted to computational or modelling tasks. This paper reports a study on students' perceptions of and difficulties with Lean, an interactive theorem prover introduced as part of a…

Concurrency is often perceived as difficult by students. One reason for this may be due to the fact that abstractions used in concurrent programs leave more situations undefined compared to sequential programs (e.g., in what order statements are executed), which makes it harder to create a proper mental model of the execution environment. Students…

Project-based assessment has been used to evaluate coding projects created by students for a long time. Nevertheless, there is a lack of rigorously tested project-based coding rubrics that are developmentally appropriate for early childhood. This study presented the development and testing of a coding rubric to evaluate children's creations with…

This exploratory study reports on characteristics of proof production and proof writing observed in the work of first-year university students who took part in workshops on the theorem prover LEAN (https://leanprover.github.io). These workshops were voluntary and offered alongside a transition to proof module in a UK university. Through…

Large language models (LLMs), such as Codex, hold great promise in enhancing programming education by automatically generating feedback for students. We investigate using LLMs to generate feedback for fixing syntax errors in Python programs, a key scenario in introductory programming. More concretely, given a student's buggy program, our goal is…

Background: Conceptual models are an essential phase in software design, but they can create confusion and reduced performance for students in Database Design courses. Objective: A novel Relational Data Model Validation Tool (MVTool) was developed and tested to determine (1) if students who use MVTool perform better than those who do not, and (2)…

The literature provides multiple measures of diversity along a single demographic dimension, but when it comes to studying the interaction of multiple diversity types (e.g. age, gender, and race), the field of useable measures diminishes. We present the use of decision trees as a machine learning technique to automatically identify the…

Programming is an essential skill that many computing students are expected to master. However, programming can be difficult to learn. Successfully interpreting compiler error messages (CEMs) is crucial for correcting errors and progressing toward success in programming. Yet these messages are often difficult to understand and pose a barrier to…

One of the most astonishing properties when studying numerical series is that the sum is not commutative, that is the sum may change when the order of its elements is altered. In this note an example is given of such a series. A well-known mathematical proof is given and a MATLAB[C] program used for different rearrangements of the series…