Skip to content

Product Updates

See the user-facing features, improvements, and fixes included in each ReasLab release.

v1.1.3

Latest
Richer AI chats and file review, plus Agent configuration and Markdown PDF export
AIAgentMarkdownPDFSettingsThemeFeedback

New Features

  • Steer and Queue Message: While the AI is still replying, Queue Message lines up follow-ups, and Steer steps into the current run right away. Queued messages can be edited, reordered, or withdrawn. Use them from the chat input; also available in Agent mode.
  • Browse and jump to past prompts with arrow keys: In the chat input, use ↑ / ↓ to cycle through prompts you already sent. Use Alt+↑ / Alt+↓ (⌥↑ / ⌥↓ on macOS) to jump to the matching user message in the conversation.
  • Export Markdown as PDF: Markdown can be exported as a same-named PDF in the same folder. Choose Export as PDF from the editor toolbar or the file-tree context menu, or ask in an AI chat to export it.
  • Customize each Agent’s internal role models and generation preferences: On the Settings page, open an Agent under Agents to assign models to its internal roles in Role models, and set generation preferences in Preferences.
  • Auto theme that follows system appearance: Theme now includes Auto, which follows your system light or dark appearance, and code highlighting follows the IDE theme more consistently. Set it under Menu → Settings.
  • Choose whether AI file edits need your approval: When Require Approval is on, AI file edits stay pending until you accept or reject them. Turn it off to accept edits automatically. Find it under Menu → Settings → AI Edits.
  • Add selected reply text to chat, or copy it: You can add selected text from an assistant reply to the chat as a quote, or copy it with Add to Chat / Copy.
  • Return to your place after following a PDF link: After jumping via an in-PDF link, you can return to where you were reading with Back to previous location, or with Alt+← (⌥← on macOS).

Improvements & Fixes

  • Chat stays closer to what you typed: Text you send is kept as typed instead of being turned into headings or lists, while code blocks still display as code. Pasted indentation and spaces are kept. Images from the web in assistant replies are no longer shown automatically.
  • Large projects open more smoothly: Projects with many files are less likely to stall when you open them. A folder that suddenly gains a large batch of files is not stored in full in project history, and very large Agent file comparisons load only after you expand them.
  • Built-in Gurobi license is now size-limited: Gurobi has restricted academic license distribution, so the built-in license changed from an unrestricted academic license to a size-limited one (about 2,000 variables and 2,000 constraints). Your own license can still be configured under Solver Settings in the sidebar.
  • Jump to Settings sections from the avatar menu: You can open Account, AI Providers, User Rules, Agents, or Tools directly from the avatar menu, without browsing Settings first.
  • TeX PDF preview no longer shows an older version while it first loads: When the TeX PDF preview first loads, or right after you switch files, it could briefly show a previous PDF. It now waits until the PDF for the current document is ready.
  • Clearer separation of public and private Feedback: When submitting Feedback, public content and private information are kept apart more clearly.
  • Review Agent file deletions before they take effect: If the Agent deletes a file, you can still review that deletion and choose to accept or reject it in the file review UI.
  • More reliable Python and Lean completions: Python and Lean language completions are more reliable in everyday editing.
  • Agent column alignment on the projects page: The Agent column on the projects page is aligned more consistently with the rest of the table.
  • Improved management of Python compute resources: Python runs now time out after 1 hour and show a timeout message. A run that did not finish normally is cleaned up so it no longer holds compute resources.
More stable Agent chats, plus clearer templates and settings
AIAgentLaTeXTemplatesSettingsCommentsOCRSolvers

New Features

  • Redesigned template library: Browse optimization, contest, and theorem-proving templates in a unified catalog that is easier to scan and start from.
  • Huawei Cup support for the Math Modeling Agent: The Math Modeling Agent now includes Huawei Cup templates and related materials for the postgraduate mathematical modeling contest, so you can start from that track more easily.
  • Support for more solvers: Modeling projects can use more solvers out of the box, including HiGHS, CBC, GLPK, and SCIP. COPT now includes a built-in platform license so you can start without configuring your own, while personal license setup is still supported. Xpress Community is also supported, and you can configure your own full license. Find them under Solver Settings in the sidebar.
  • Redesigned user settings: Account, AI Providers, User Rules, and related preferences are gathered into one page with clearer navigation. Open it from Settings in the editor sidebar, or from Settings in the avatar menu.
  • More flexible OCR control: You can turn off automatic text extraction for images and PDFs attached in AI chats, and click OCR on a file when you need it (Menu → Settings → Auto OCR). You can also right-click an image or PDF in the file tree or preview and choose OCR to Markdown; the result is saved as a same-named Markdown file in the same folder.
  • Fork a chat from any assistant reply: Any assistant reply can be used as a checkpoint: fork from that point to continue in a new chat without losing the earlier context.

Improvements & Fixes

  • Long Agent chats are much less likely to crash the page: Long-running Agent conversations are far less likely to freeze or crash the browser while replies are streaming, when you expand a tool result, or when you reopen a long history.
  • Safer and faster review of large file edits: Rejecting a large Agent edit no longer risks deleting a file you already had. Accepting or rejecting changes also no longer takes tens of seconds.
  • New Agent conversations become ready sooner: Starting a new Agent conversation no longer adds a few seconds of waiting. If startup fails, you see an error right away instead of a conversation that looks stuck.
  • Support recompiling TeX with Ctrl+S / ⌘+S: In a TeX file, press Ctrl+S / ⌘+S to recompile, without looking for the compile button.
  • Comments without interrupting your layout: You can add a comment without the review panel jumping open, and the comment popup stays on screen even when you select text near the edge of the editor.
More reliable collaboration and long conversations
CollaborationAI

Improvements & Fixes

  • Edits land where you expect in collaborative files: Files that use Windows-style line endings are now handled consistently during collaborative editing, so typed changes stay on the line you see instead of shifting after save or reload.
  • Longer conversations stay usable as they grow: Context compression now accounts for the context window of each model more accurately, keeps a larger recent portion of the conversation when the window allows, and continues with a simpler summary if the usual compression step fails, so long sessions are less likely to get stuck.
Rethlas, a new default model, and a more polished IDE
AIModelsAuthenticationIDELeanProjects

Special Notice

  • On the stability of AI conversations: We have heard from a number of you that AI conversations have sometimes been slow to respond or have stopped partway through. This mainly traces back to recent fluctuations in the upstream service behind ReasPro and ReasProX. We are already working on improvements and will keep a close watch on service quality. In the meantime, switching to deepseek-flash should give you a smoother experience. Thank you for letting us know, and for bearing with us.

New Features

  • Rethlas proof agent: Rethlas is now available for research-level mathematical proof generation, with independent verification and repair built into its workflow.
  • deepseek-flash is the new default model: New conversations now use deepseek-flash by default. You can still switch to any other available model at any time from model settings.
  • Reasoning options that match the model you pick: The Chain of Thought control now shows only the options the selected model actually supports, so you can turn thinking on or off, choose how much effort it spends, or leave it on Auto to follow the model default.
  • Open project files from AI responses: Links to files in the current workspace can now be opened directly from ReasLingo responses and Markdown previews, making it easier to move from an AI explanation to the relevant source.
  • More ReasLab products in Discovery: ReaScholar, an academic search tool for exploring research literature and methods, and OptBound, a unified benchmark of lower and upper complexity bounds in optimization, are now available from the ReasLab homepage.

Improvements & Fixes

  • No more conversations stuck on receiving a reply: Fixed cases where a conversation kept showing that it was still receiving a reply after the response had already finished or failed.
  • ReasFlow Agent works with the model you selected: ReasFlow Agent no longer restricts which model it accepts, so sending a message no longer fails with a model-compatibility warning.
  • Clearer OCR limits without losing attachments: Oversized images and PDFs remain attached even when OCR is skipped, while PDFs longer than 20 pages clearly indicate that only the first 20 pages will be processed.
  • Clearer sign-up and account recovery feedback: Verification emails, magic links, and password reset requests now show clearer success and error states, resend countdowns, and more helpful expired-link guidance.
  • More reliable Agent context compression: Long-running Agent tasks now compress their history more reliably and recover instead of stopping when a conversation outgrows the model context window.
  • Better browser compatibility for PDF previews: Improved PDF preview compatibility to address cases where documents could not be displayed correctly in older browsers.
  • More reliable Lean project setup: Improved dependency-cache repair and recovery for missing ProofWidgets assets, reducing setup failures in Lean projects.
  • Fewer Playground and Infoview errors: Opening a file in Playground no longer reports an error before the editor content is ready, and reopening the same file repeatedly no longer leaves the Lean language service in a broken state.
  • Refined dark theme and IDE layout: Extended dark theme coverage across the IDE, aligned file tree and Infoview colors with the editor, kept collapsed folders closed when a file is opened, and tidied the ReasLingo panel at narrow widths.
  • Smoother project creation: Creating a project no longer briefly shows a name-already-taken warning while the project is being created, and the create button stays disabled until it finishes to prevent duplicate projects.
  • Large Python outputs no longer break the editor: Execution results are no longer allowed to fill up browser storage, so scripts that produce a lot of output no longer cause errors or lose open tabs and session state.
  • Clearer template details when no paper is included: Template details now state when a template has no reference paper, instead of showing a preview that never finishes loading, and the tabs keep a consistent size and hover style.
  • No duplicate AI chats from your own share links: Opening a project share link you created no longer imports a second copy of your existing AI conversations.
  • Smoother project and collaborator management: Made the remove-member action easier to find, improved Git import failure details, and strengthened cleanup of deleted project data.
More reliable uploads and collaboration
ProjectsCollaborationPDF

New Features

  • Clickable links in PDF previews: External links embedded in LaTeX-generated PDFs can now be opened directly from the built-in preview.

Improvements & Fixes

  • More resilient file uploads and ZIP imports: Project files and ZIP archives now use a unified upload flow with clearer progress, stronger error handling, and retry support for failed files.
  • More reliable collaborative editing: Fixed remote collaborator cursors and strengthened document synchronization so shared editing state remains accurate across participants.
  • Better handling of very large project files: Large generated data files no longer enter the real-time collaboration pipeline unnecessarily, reducing background work and improving project stability.
  • Clearer AI session titles: Improved automatic conversation title generation so sessions are easier to recognize and revisit.
More reliable AI sessions
AIPerformanceReliability

Improvements & Fixes

  • More efficient long conversations: Optimized how ReasLingo conversations are saved, reducing redundant background work as sessions grow and improving the reliability of long-running chats.
  • Quieter idle sessions: Idle conversations no longer wake periodically when nothing has changed, reducing unnecessary background activity.
Smoother imports, nested Lean projects, and IPOPT
LeanGitOptimizationOCR

New Features

  • Nested Lean project support: ReasLab can now detect and open a Lean workspace located in a project subdirectory, with the active workspace root shown during setup and editing.
  • IPOPT solver: IPOPT is now available in the optimization solver settings alongside the existing solver integrations.

Improvements & Fixes

  • Clearer Git import and Lean setup progress: Redesigned project import and setup feedback makes each stage easier to follow, with clearer progress, errors, logs, and retry actions.
  • Larger PDF inputs for OCR: Raised the supported PDF size limit for OCR workflows so larger research documents can be processed directly.
  • Cleaner announcements and status information: Refined notification dialogs, maintenance messages, and the IDE status area for a more consistent experience.
  • Cleaner Python outputs: Python execution no longer leaves an empty images directory when a task does not generate images.
Generated LaTeX files, JSON editing, and collaborator controls
LaTeXEditorCollaborationLean

New Features

  • Download generated LaTeX files: Files produced during LaTeX builds can now be downloaded from the IDE, making it easier to inspect and reuse generated artifacts.
  • JSON editing and formatting: JSON files now have dedicated syntax support and formatting, with clearer JSON output in tool results.
  • Remove project collaborators: Project owners and administrators can remove collaborators directly from project settings.

Improvements & Fixes

  • More reliable Lean setup: Lean packages whose names contain escaped characters are now normalized correctly during project setup.
  • Clearer system update notices: Improved the presentation of system update and maintenance messages so their status and timing are easier to understand.
Faster LaTeX editing and more reliable previews
LaTeXPDFCollaborationAnnouncements

Improvements & Fixes

  • PDF previews stay current: The PDF preview now refreshes correctly after compilation, including builds initiated by an AI agent.
  • More responsive LaTeX completion: Reduced completion latency while typing and avoided unnecessary preview updates during editing.
  • More reliable collaborative sync: Improved document synchronization for slower or larger collaborative sessions to reduce avoidable timeouts.
  • Less interference between AI editing and live preview: Separated agent-driven editor updates from the LaTeX live-preview lifecycle for a steadier editing experience.
  • Refined announcement view: Improved the layout and readability of in-product announcements.
System announcements and smoother authoring
AnnouncementsLaTeXMarkdownAgent

New Features

  • In-product system announcements: ReasLab can now present product updates, service notices, and maintenance information directly in the application.
  • OptAgent availability: OptAgent can now be selected for supported production optimization workflows.

Improvements & Fixes

  • Faster and more stable LaTeX assistance: Reduced completion latency and fixed several TexLab issues that could interrupt authoring assistance.
  • More reliable Markdown previews: External asset links no longer trigger a reload loop, and Mermaid diagrams render at their intended size.
  • Quokka opens without leaving ReasLab: Quokka navigation now opens in a new tab so the current ReasLab project page remains available.
ReasFlow and faster PDF viewing
ReasFlowPDFPlayground

New Features

  • ReasFlow paper copilot: ReasFlow is now available in ReasLab for AI-assisted research writing and paper workflows.

Improvements & Fixes

  • Faster large-document PDF previews: PDF pages are rendered as they enter view, reducing initial load work for longer documents.
  • Less repetitive Playground guidance: Dismissing the Playground introduction now keeps it hidden for the current browser session.
A stronger LaTeX workflow and more dependable projects
LaTeXPDFLeanProjects

New Features

  • Expanded LaTeX authoring tools: Added a dedicated authoring toolbar, build-target selection, project-wide bibliography completion, foldable sections, and outline expand/collapse controls.
  • Improved PDF reading controls: Added fit-width and actual-size switching, safer zoom limits, horizontal scrolling for zoomed pages, and a presentation view.
  • Math Modeling Agent: The Math Modeling Agent is now available for supported modeling workflows.

Improvements & Fixes

  • More reliable LaTeX builds: Builds now provide clearer failure details, support cancellation, refresh previews after agent-generated output, and recover more gracefully when language services become unresponsive.
  • Safer project sharing and collaboration: Strengthened sharing permission checks and improved initial synchronization for collaborative documents.
  • Smoother project import and export: Git imports can be renamed when a project name is already taken, and Lean project metadata is preserved in ZIP uploads and downloads.
Agent mode, performance upgrades, and new products
PerformanceAgentEditorLeanNew Products

New Features

  • Brand-new Agent mode: Introduces Agent mode for complex tasks. AI can break down requirements, edit across files, run commands in an isolated environment, and show its progress through the Activity panel. You can switch back to Editor mode at any time.
  • Multi-dimensional context references: Use @ in the input box to search for project files or directories, or drag files from the file tree into the conversation in both Agent and Editor modes.
  • LaTeX intelligent compile flow: Automatic LaTeX compiler selection improves compilation for projects that use different engines.
  • New product: Quokka: Quokka converts mathematical textbooks, papers, and other natural-language material into compilable Lean projects through automatic decomposition, translation, and iterative repair.
  • New product: Arena: OptArena provides a public benchmark platform for evaluating multimodal language models on optimization modeling tasks.

Improvements & Fixes

  • Performance architecture upgrade: System architecture and session management improvements deliver faster responses, better support for concurrent use, and quicker loading of conversation history.
  • Lean performance and collaboration: Improved Lean language-server responsiveness and the real-time multi-user editing experience.

v1.0.0-rc.1

Pre-release
Smoother long AI responses
AIPerformanceMarkdown

Improvements & Fixes

  • More responsive long AI messages: Large and continuously streaming agent responses now remain smoother by rendering only the content currently in view and avoiding repeated work for completed blocks.
  • Improved Markdown math rendering: Bracketed display-math syntax is now rendered correctly as a block formula.
  • Small interaction fixes: Improved narrow-panel search controls and preserved interactions in the conversation deletion dialog.

preview

Pre-release
Public Preview
AILeanCollaborationIDE

New Features

  • ReasLingo embedded AI assistant: An AI assistant integrated into the IDE workflow, with custom providers, tool calls, code diff review, multimodal OCR, web search, reasoning controls, user rules, and shareable sessions.
  • Lean 4 cloud formal proof environment: A ready-to-use Lean 4 environment with version switching, package management, Infoview, language services, semantic search, Mathlib project builds, and a lightweight Playground.
  • Academic document engine: LaTeX and Markdown authoring with multiple TeX engines, PDF preview, SyncTeX navigation, structured diagnostics, mathematical typesetting, and syntax highlighting.
  • Python and optimization modeling: Isolated Python execution, fast package management, integrated commercial solvers, execution history, and modeling templates.
  • Real-time collaboration and project management: Conflict-free collaborative editing, collaborator presence, project permissions, GitHub import, snapshots, visual diffs, rollback, and reusable templates.