AG 1, AG 2, AG 3, INET, AG 4, AG 5, D6, SWS, RG1, MMCI   Info

AG Audience

English

30 Minutes

Research in program comprehension has shown that reading common programming code primarily activates language-related brain regions. In contrast, mathematical reasoning involves distinct neural pathways, as revealed by studies of mathematicians’ cognitive processes. This disparity raises fundamental questions when we consider theorem-proving programs, which sit at the intersection of programming and mathematical reasoning: What cognitive processes are involved when understanding proof code? How do programming experts and mathematics experts differ in their approaches to proof understanding? Moreover, how can we measure and address the cognitive challenges novices face in this domain? The answers to these questions could guide us in enhancing how we display context for theorem proving. In proof development, context refers to the collection of available information at any given point—including variables, their types, assumptions, and proof goals—that helps programmers understand where they are and what they can do next. Current proof assistants primarily present context through textual notation of elements and types. However, neuroscience research on expert mathematicians suggests that advanced mathematical thinking predominantly utilizes neural circuits for spatial and numerical processing rather than language areas. This indicates that when we struggle to understand the text of a program, we might be missing crucial spatial and numerical information— which can be seen as a form of potential context. For instance, in SK combinator calculus, functions are represented as strings containing only ‘S’ and ‘K’, which are difficult to comprehend in their textual form, but become much clearer when visualized as binary trees. Additionally, research on programmer efficacy reveals that expert programmers demonstrate more targeted code-reading patterns with lower cognitive load. This experience-driven selective attention represents another potential context that could be made explicit in proof development environments. By investigating where programming and mathematical cognition meet in formalization, I aim to identify the true context for understanding theorem proving - a context that exists both within and beyond the code itself. This context will be made visible through not only text, but also diagrams, and thought structures that guide program understanding. This research will inform the design of next-generation proof assistants that bridge the gap between programming and mathematical reasoning, making formal methods more accessible to everyone.

Ina Geisler

+49 681 9325 1802

--email hidden

Zoom

passcode not visible

logged in users only