CAREER: Patterns and Toolkits for Making Scientific Notation and Formal Proof Understandable through Interaction

Some of the most powerful ideas in STEM are expressed in symbols, equations, and proofs. Unfortunately, these formal representations (i.e., formalisms) can be hard to understand, putting distance between millions of learners, practitioners, and scientists and the concepts that could support their work. The fact that scientific texts are becoming increasingly digital provides new opportunities to help readers understand formalisms. Digital texts might let readers look at individual terms in equations, access definitions that are aligned with their own knowledge, and see examples that make their meanings more concrete. However, creating these expanded ways of engaging with formalisms can be difficult for authors, and it is not clear which kinds of support would be most helpful to readers. This project looks to address these questions by developing a design space of ways to better-explain formalisms, tools for authors to create and readers to use these explanations, and studies of how these explanations help authors and readers talk and learn about science. By doing the work with both scientists and students, the project will lower barriers to those struggling with equations and proofs, leading to better STEM education and a stronger STEM workforce. This project's contribution is the design of, evaluation of, and tools for creating "explorable formalisms". These are formal representations, including symbols, equations, and proof, that are made more intelligible through interaction. The research will first contribute interaction techniques for making formalisms' meaning clear through interaction, for instance with on-demand diagrams, walkthroughs, simulations, and logical traces. Second, the research team will provide empirical evidence of the usefulness of the techniques grounded in studies of learning in the lab and classroom. Third, the researchers will develop new tools to facilitate the creation of explorable formalisms. These include a new markup language for rapidly and cleanly associating textual and LaTeX formalisms with granular descriptions, computations, and presentation hints. They also include algorithms supporting equation diagram layout and logical trace discovery. To bring explorable formalisms to scientific texts broadly, this project disseminates the tools, pilots their integration into AI-based systems for answering scientific questions, and incorporates them into learning materials for STEM classrooms. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria. NSF Award ID: 2541577 | Program: 01002627DB NSF RESEARCH & RELATED ACTIVIT,01002930DB NSF RESEARCH & RELATED ACTIVIT,01003031DB NSF RESEARCH & RELATED ACTIVIT | Principal Investigator: Andrew Head | Institution: University of Pennsylvania, PHILADELPHIA, PA | Award Amount: $400,807 View on NSF Award Search: https://www.nsf.gov/awardsearch/show-award/?AWD_ID=2541577 View on Research.gov: https://www.research.gov/awardapi-service/v1/awards/2541577.html