Explorable Theorems: Making Written Theorems Explorable by Grounding Them in Formal Representations

arXiv (Cornell University) · 2026-04-03

LLM-generated explanations can make technical content more accessible, but there is a ceiling on what they can support interactively. Because LLM outputs are static text, they cannot be executed or stepped through. We argue that grounding explanations in a formalized representation enables interactive affordances beyond what static text supports. We instantiate this idea for mathematical proof comprehension with explorable theorems, a system that uses LLMs to translate a theorem and its written proof into Lean, a programming language for machine-checked proofs, and links the written proof with the Lean code. Readers can work through the proof at a step-level granularity, test custom examples or counterexamples, and trace the logical dependencies bridging each step. Each worked-out step is produced by executing the Lean proof on that example and extracting its intermediate state. A user study ($n = 16$) shows potential advantages of this approach: in a proof-reading task, participants who had access to the provided explorability features gave better, more correct, and more detailed answers to comprehension questions, demonstrating a stronger overall understanding of the underlying mathematics.

LitPivot: Developing Well-Situated Research Ideas Through Dynamic Contextualization and Critique within the Literature Landscape

arXiv (Cornell University) · 2026-04-03

Developing a novel research idea is hard. It must be distinct enough from prior work to claim a contribution while also building on it. This requires iteratively reviewing literature and refining an idea based on what a researcher reads; yet when an idea changes, the literature that matters often changes with it. Most tools offer limited support for this interplay: literature tools help researchers understand a fixed body of work, while ideation tools evaluate ideas against a static, pre-curated set of papers. We introduce literature-initiated pivots, a mechanism where engagement with literature prompts revision to a developing idea, and where that revision changes which literature is relevant. We operationalize this in LitPivot, where researchers concurrently draft and vet an idea. LitPivot dynamically retrieves clusters of papers relevant to a selected part of the idea and proposes literature-informed critiques for how to revise it. A lab study ($n{=}17$) shows researchers produced higher-rated ideas with stronger self-reported understanding of the literature space; an open-ended study ($n{=}5$) reveals how researchers use LitPivot to iteratively evolve their own ideas.

Large-scale human predictions of the replicability of published social and behavioural science papers – a multi- study analysis

2026-04-01 · 2 citations

This paper reports two approaches to forecasting replicability for a corpus of 3000 published social science papers, using large-scale human assessments. Replication Markets used incentivized surveys and prediction markets where participants traded assets linked to replication outcomes and market prices were interpreted as replication predictions. The repliCATS project used a structured group deliberation protocol, including interactive discussion, and mathematically aggregated forecasts to generate replication predictions. Accuracy for both approaches was validated against a subset of (n=37) independent, high-power replication studies. The predictive accuracy (median [range]) achieved for AUC by Replication Markets was 0.76 [0.72-0.82], and 0.76 [0.68-0.81] by repliCATS. Replication Markets achieved a classification accuracy of 73% [68-76%] and repliCATS achieved 68% [59-78%]. These results place the performance of both teams within the accuracy range achieved in prior replication forecasting studies. We conclude that informative forecasts can be elicited by both methods, but there are trade-offs between scale and accuracy.

Connecting the Dots: Surfacing Structure in Documents through AI-Generated Cross-Modal Links

Open MIND · 2026-02-18

Understanding information-dense documents like recipes and scientific papers requires readers to find, interpret, and connect details scattered across text, figures, tables, and other visual elements. These documents are often long and filled with specialized terminology, hindering the ability to locate relevant information or piece together related ideas. Existing tools offer limited support for synthesizing information across media types. As a result, understanding complex material remains cognitively demanding. This paper presents a framework for fine-grained integration of information in complex documents. We instantiate the framework in an augmented reading interface, which populates a scientific paper with clickable points on figures, interactive highlights in the body text, and a persistent reference panel for accessing consolidated details without manual scrolling. In a controlled between-subjects study, we find that participants who read the paper with our tool achieved significantly higher scores on a reading quiz without evidence of increased time to completion or cognitive load. Fine-grained integration provides a systematic way of revealing relationships within a document, supporting engagement with complex, information-dense materials.

LitPivot: Developing Well-Situated Research Ideas Through Dynamic Contextualization and Critique within the Literature Landscape

ArXiv.org · 2026-04-03

Developing a novel research idea is hard. It must be distinct enough from prior work to claim a contribution while also building on it. This requires iteratively reviewing literature and refining an idea based on what a researcher reads; yet when an idea changes, the literature that matters often changes with it. Most tools offer limited support for this interplay: literature tools help researchers understand a fixed body of work, while ideation tools evaluate ideas against a static, pre-curated set of papers. We introduce literature-initiated pivots, a mechanism where engagement with literature prompts revision to a developing idea, and where that revision changes which literature is relevant. We operationalize this in LitPivot, where researchers concurrently draft and vet an idea. LitPivot dynamically retrieves clusters of papers relevant to a selected part of the idea and proposes literature-informed critiques for how to revise it. A lab study ($n{=}17$) shows researchers produced higher-rated ideas with stronger self-reported understanding of the literature space; an open-ended study ($n{=}5$) reveals how researchers use LitPivot to iteratively evolve their own ideas.

Science and Technology for Augmenting Reading (STAR)

2026-04-13

The landscape of technology for consuming information is changing rapidly. One mode of information consumption, reading, stands to see profound changes due to its ubiquity and frequency as a cognitive task. Better reading technology could transform texts on demand so that they are easier to read, surface hard-to-find information, support synthesis, and better engage readers. The possibilities have been considerably expanded with the maturation of AI. The purpose of this workshop is to provide a platform for the growing cohort of HCI and AI researchers interested in augmented reading interfaces to define high-impact areas of development and standards of success. This platform will arise from two components of our workshop. The first is a brief and engaging format of introductions among community members through lightning talks. The second is a set of affinity group activities that will identify fresh opportunities for augmenting reading against the backdrop of reading theories, evaluation practices, and emerging technology.

Explorable Theorems: Making Written Theorems Explorable by Grounding Them in Formal Representations

ArXiv.org · 2026-04-03

LLM-generated explanations can make technical content more accessible, but there is a ceiling on what they can support interactively. Because LLM outputs are static text, they cannot be executed or stepped through. We argue that grounding explanations in a formalized representation enables interactive affordances beyond what static text supports. We instantiate this idea for mathematical proof comprehension with explorable theorems, a system that uses LLMs to translate a theorem and its written proof into Lean, a programming language for machine-checked proofs, and links the written proof with the Lean code. Readers can work through the proof at a step-level granularity, test custom examples or counterexamples, and trace the logical dependencies bridging each step. Each worked-out step is produced by executing the Lean proof on that example and extracting its intermediate state. A user study ($n = 16$) shows potential advantages of this approach: in a proof-reading task, participants who had access to the provided explorability features gave better, more correct, and more detailed answers to comprehension questions, demonstrating a stronger overall understanding of the underlying mathematics.

The Invisible Mentor: Inferring User Actions from Screen Recordings to Recommend Better Workflows

2026-04-13

Users of feature-rich tools like Excel often miss more efficient workflows, repeating tedious steps and making avoidable errors. Current approaches to helping them require either manual prompting, which is effortful for users, or automated logging, which is limiting for developers. We present InvisibleMentor, a system inspired by over-the-shoulder learning: it observes what users do, then shows them how to do it better. To do this, InvisibleMentor analyzes screen recordings with a vision-language model to reconstruct actions and context, then uses a large language model to generate vision-grounded task reflection, structured suggestions grounded in observed behavior. In a user study, participants found InvisibleMentor’s suggestions more clear, more relevant, and more useful than those from a prompt-based assistant, demonstrating that AI can do more than automate away work—it can help users master it.

Connecting the Dots: Surfacing Structure in Documents through AI-Generated Cross-Modal Links

arXiv (Cornell University) · 2026-02-18

Understanding information-dense documents like recipes and scientific papers requires readers to find, interpret, and connect details scattered across text, figures, tables, and other visual elements. These documents are often long and filled with specialized terminology, hindering the ability to locate relevant information or piece together related ideas. Existing tools offer limited support for synthesizing information across media types. As a result, understanding complex material remains cognitively demanding. This paper presents a framework for fine-grained integration of information in complex documents. We instantiate the framework in an augmented reading interface, which populates a scientific paper with clickable points on figures, interactive highlights in the body text, and a persistent reference panel for accessing consolidated details without manual scrolling. In a controlled between-subjects study, we find that participants who read the paper with our tool achieved significantly higher scores on a reading quiz without evidence of increased time to completion or cognitive load. Fine-grained integration provides a systematic way of revealing relationships within a document, supporting engagement with complex, information-dense materials.

Towards Caregiver-Centric Health Technology in Intricate Care Situations

2026-04-13

This work serves to inform the design of better health information technology for intricate care scenarios. We focus on a situation involving a severe condition, child patients, rich know-how, and complex caregiver networks—childhood asthma in our local urban community. Conducting design investigations with 23 caregivers who are predominantly Black and single across 14 interviews and 2 workshop sessions, we offer the following observations. First, caregivers draw on rich knowledge about triggers, mitigations, and medication, which often reflect medical consensus, but occasionally conflict. Second, asthma care involves acute, highly stressful episodes, exemplified by caregivers’ nighttime monitoring and management. Third, care systems are distributed among parent, child, broader family, and schools. This leads to decentralized information and responsibility, communication needs, and concerns around reliability of care. We conclude if health technology is to support this situation, it will mind community knowledge, intense acute episodes, and the decentralized and heterogeneous nature of care.