diff --git a/TeXmacs/packages/standard/std-math.ts b/TeXmacs/packages/standard/std-math.ts
index a7254f41d4..df9b70f66e 100644
--- a/TeXmacs/packages/standard/std-math.ts
+++ b/TeXmacs/packages/standard/std-math.ts
@@ -161,6 +161,25 @@
 
   <assign|cfrac|<macro|x|y|<with|mode|math|<dfrac|<arg|x>|<resize|<arg|y>|||<plus|1r|-1sep>|>>>>>
 
+  <\comment>
+    Proof tree macros: wrap tree primitive with tree-mode=proof
+    - proof-tree: no label
+    - proof-tree*: label on right
+    - proof-tree**: label on left
+  </comment>
+
+  <assign|proof-tree|<macro|body|<with|tree-mode|proof|<arg|body>>>>
+
+  <assign|proof-tree*|<macro|body|<with|tree-mode|proof|tree-label-pos|right|<arg|body>>>>
+
+  <assign|proof-tree**|<macro|body|<with|tree-mode|proof|tree-label-pos|left|<arg|body>>>>
+
+  <drd-props|proof-tree|arity|1>
+
+  <drd-props|proof-tree*|arity|1>
+
+  <drd-props|proof-tree**|arity|1>
+
   <assign|frac*|<macro|x|y|<move|<lsup|<arg|x>><resize|/|<plus|1l|0.15em>|<plus|1b|0.5em>|<minus|1r|0.15em>|<minus|1t|0.5em>><rsub|<arg|y>>||0.05em>>>
 
   <drd-props|frac*|arity|2|syntax|<macro|x|y|<arg|x>/<arg|y>>>
diff --git a/TeXmacs/progs/generic/generic-edit.scm b/TeXmacs/progs/generic/generic-edit.scm
index 37a716485c..86eda335a6 100644
--- a/TeXmacs/progs/generic/generic-edit.scm
+++ b/TeXmacs/progs/generic/generic-edit.scm
@@ -338,6 +338,7 @@
   (or (tree-in? t '(tree))
       (table-markup-context? t)))
 
+
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; Focus predicates
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -767,6 +768,421 @@
   (:require (tree-is? t 'tree))
   (go-to-repeat (if downwards? structured-down structured-up)))
 
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Proof tree editing
+;; Note: proof-tree is now a macro that wraps tree with tree-mode=proof
+;; The structure is: (with tree-mode proof (tree conclusion premise1 premise2 ...))
+;; For labeled: (with tree-mode proof tree-label-pos right (tree label conclusion premise1 ...))
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+;; Find the enclosing 'with' tag that sets tree-mode=proof
+(tm-define (find-proof-tree-with t)
+  (cond
+    ((not (tree? t)) #f)
+    ((and (tree-is? t 'with)
+          (>= (tree-arity t) 3)
+          (tm-equal? (tree-ref t 0) "tree-mode")
+          (tm-equal? (tree-ref t 1) "proof"))
+     t)
+    (else (find-proof-tree-with (tree-up t)))))
+
+(tm-define (get-proof-tree-label-pos with-t)
+  ;; Get the current label position from the with tag
+  ;; Returns "none", "right", or "left"
+  (if (and (>= (tree-arity with-t) 5)
+           (tm-equal? (tree-ref with-t 2) "tree-label-pos"))
+      (tm->string (tree-ref with-t 3))
+      "none"))
+
+;; Check if t is a tree in proof-tree mode
+(tm-define (proof-tree-tag? t)
+  (and (tree-is? t 'tree)
+       (find-proof-tree-with t)))
+
+;; Check if the proof-tree has a label
+(define (proof-tree-labeled? t)
+  (and (proof-tree-tag? t)
+       (and-with with-t (find-proof-tree-with t)
+         (let ((pos (get-proof-tree-label-pos with-t)))
+           (or (== pos "left") (== pos "right"))))))
+
+;; Check if label is on the left
+(define (proof-tree-label-left? t)
+  (and-with with-t (find-proof-tree-with t)
+    (== (get-proof-tree-label-pos with-t) "left")))
+
+;; Predicate: are we inside a proof-tree?
+;; Uses get-env-tree to check cursor's environment
+(define (inside-proof-tree?)
+  (and (tree-innermost 'tree)
+       (tm-equal? (get-env-tree "tree-mode") "proof")))
+
+(define (proof-tree-premise-start t)
+  ;; Return the index of the first premise
+  (if (proof-tree-labeled? t) 2 1))
+
+(define (proof-tree-conclusion-idx t)
+  ;; Return the index of the conclusion
+  (if (proof-tree-labeled? t) 1 0))
+
+(define (proof-tree-cycle-label-pos current forward?)
+  ;; Return the next label position in the cycle
+  (let ((order (if forward?
+                   '("none" "right" "left")
+                   '("none" "left" "right"))))
+    (let loop ((l order))
+      (cond
+        ((null? l) "none")
+        ((null? (cdr l)) (car order))
+        ((== (car l) current) (cadr l))
+        (else (loop (cdr l)))))))
+
+(tm-define (proof-tree-set-variant with-t new-pos)
+  ;; Set the proof-tree variant by modifying with tag and tree structure
+  ;; All proof-trees have tree-label-pos (either "none", "left", or "right")
+  ;; Tree is always at index 4 in the with tag
+  (let* ((current-pos (get-proof-tree-label-pos with-t))
+         (tree-t (tree-ref with-t 4)))
+    (when (tree-is? tree-t 'tree)
+      (cond
+        ;; From no label to labeled: add label child to tree, set position value
+        ((and (== current-pos "none") (!= new-pos "none"))
+         (tree-insert! tree-t 0 '(""))
+         (tree-set (tree-ref with-t 3) new-pos))
+        ;; From labeled to no label: remove label child, set position to "none"
+        ((and (!= current-pos "none") (== new-pos "none"))
+         (tree-remove! tree-t 0 1)
+         (tree-set (tree-ref with-t 3) "none"))
+        ;; Change label side (left <-> right): just change the value
+        ((and (!= current-pos "none") (!= new-pos "none"))
+         (tree-set (tree-ref with-t 3) new-pos))))))
+
+;; Helper function to set proof-tree label from the focused tree
+(tm-define (proof-tree-set-label-pos t new-pos)
+  (and-with with-t (find-proof-tree-with t)
+    (proof-tree-set-variant with-t new-pos)))
+
+;; Get current label position from focused tree
+(tm-define (proof-tree-current-label-pos t)
+  (and-with with-t (find-proof-tree-with t)
+    (get-proof-tree-label-pos with-t)))
+
+(tm-define (variant-circulate t forward?)
+  (:require (proof-tree-tag? t))
+  (and-with with-t (find-proof-tree-with t)
+    (let* ((current-pos (get-proof-tree-label-pos with-t))
+           (new-pos (proof-tree-cycle-label-pos current-pos forward?)))
+      (proof-tree-set-variant with-t new-pos))))
+
+;; Navigation for proof-tree:
+;; - kbd-left/kbd-right: use default behavior (works correctly now)
+;; - kbd-up/kbd-down: jump between conclusion and premises
+;; - structured-left/right: move between premises only
+;; - structured-up/down: same as kbd-up/down
+
+;; Helper to get cursor position within proof-tree
+(define (proof-tree-cursor-child-index pt)
+  (tree-down-index pt))
+
+;; Structured horizontal navigation: only moves between premises
+(define (proof-tree-navigate-horizontal pt forwards?)
+  (let* ((prem-start (proof-tree-premise-start pt))
+         (i (proof-tree-cursor-child-index pt))
+         (n (tree-arity pt)))
+    (when (and i (>= i prem-start))
+      (cond
+        ((and forwards? (== i (- n 1)))
+         (tree-go-to pt :end))
+        ((and forwards? (< i (- n 1)))
+         (tree-go-to pt (+ i 1) :start))
+        ((and (not forwards?) (== i prem-start))
+         (noop))
+        ((and (not forwards?) (> i prem-start))
+         (tree-go-to pt (- i 1) :end))))))
+
+;; Helper: find the innermost proof-tree within a tree (for drilling down)
+(define (find-innermost-proof-tree-conclusion t)
+  ;; If t is a proof-tree, go to its conclusion and recurse
+  ;; Otherwise return #f
+  (cond
+    ((proof-tree-tag? t)
+     (let* ((conc-idx (proof-tree-conclusion-idx t))
+            (conc (tree-ref t conc-idx)))
+       ;; Check if conclusion itself contains a proof-tree
+       (or (find-innermost-proof-tree-conclusion conc)
+           ;; Otherwise return this conclusion path
+           (begin (tree-go-to t conc-idx :start) #t))))
+    ((and (tree? t) (> (tree-arity t) 0))
+     ;; Search children for proof-tree
+     (let loop ((i 0))
+       (if (>= i (tree-arity t))
+           #f
+           (or (find-innermost-proof-tree-conclusion (tree-ref t i))
+               (loop (+ i 1))))))
+    (else #f)))
+
+;; Helper: find parent proof-tree that contains current pt as a premise
+(define (find-parent-proof-tree pt)
+  ;; Go up the tree to find a proof-tree ancestor where pt is a premise
+  (and-with parent (tree-up pt)
+    (if (proof-tree-tag? parent)
+        (let* ((prem-start (proof-tree-premise-start parent))
+               (idx (tree-index pt)))
+          (if (and idx (>= idx prem-start))
+              parent  ;; pt is a premise of parent
+              #f))    ;; pt is conclusion or label, not a premise
+        (find-parent-proof-tree parent))))
+
+;; Enhanced vertical navigation:
+;; UP in conclusion -> go to closest premise, drill into nested proof-tree conclusions
+;; DOWN in conclusion -> if we're a premise of parent, go to parent's conclusion
+(define (proof-tree-navigate-vertical pt to-premises?)
+  (let* ((prem-start (proof-tree-premise-start pt))
+         (conc-idx (proof-tree-conclusion-idx pt))
+         (i (proof-tree-cursor-child-index pt)))
+    (when i
+      (cond
+        ;; In conclusion, go UP to first premise
+        ((and to-premises? (== i conc-idx))
+         (let ((prem (tree-ref pt prem-start)))
+           ;; If premise is/contains a proof-tree, drill into its conclusion
+           (if (not (find-innermost-proof-tree-conclusion prem))
+               ;; No nested proof-tree, just go to the premise
+               (tree-go-to pt prem-start :start))))
+        ;; In premise, go DOWN to conclusion
+        ((and (not to-premises?) (>= i prem-start))
+         (tree-go-to pt conc-idx :start))
+        ;; In conclusion, go DOWN to parent's conclusion (if we're a premise)
+        ((and (not to-premises?) (== i conc-idx))
+         (and-with parent-pt (find-parent-proof-tree pt)
+           (let ((parent-conc-idx (proof-tree-conclusion-idx parent-pt)))
+             (tree-go-to parent-pt parent-conc-idx :start))))
+        ;; In label, go to premises (UP) or conclusion (DOWN)
+        ((and (proof-tree-labeled? pt) (== i 0))
+         (if to-premises?
+             (tree-go-to pt prem-start :start)
+             (tree-go-to pt conc-idx :start)))))))
+
+;; Override kbd-vertical for proof-tree nodes
+;; This is called when traversing up from focus-tree
+(tm-define (kbd-vertical t downwards?)
+  (:require (proof-tree-tag? t))
+  ;; downwards? means DOWN key, so to-premises? = (not downwards?)
+  (proof-tree-navigate-vertical t (not downwards?)))
+
+;; Override structured-left/right/up/down to find proof-tree ancestor
+(tm-define (structured-left)
+  (:require (inside-proof-tree?))
+  (with pt (tree-innermost 'tree)
+    (proof-tree-navigate-horizontal pt #f)))
+
+(tm-define (structured-right)
+  (:require (inside-proof-tree?))
+  (with pt (tree-innermost 'tree)
+    (proof-tree-navigate-horizontal pt #t)))
+
+;; Override structured-vertical for proof-tree nodes
+(tm-define (structured-vertical t downwards?)
+  (:require (proof-tree-tag? t))
+  ;; downwards? means DOWN, so to-premises? = (not downwards?)
+  (proof-tree-navigate-vertical t (not downwards?)))
+
+;; Insert/remove helpers for proof-tree
+(define (proof-tree-insert-horizontal pt forwards?)
+  (let* ((prem-start (proof-tree-premise-start pt))
+         (i (proof-tree-cursor-child-index pt)))
+    ;; Only insert when in premises area
+    (when (and i (>= i prem-start))
+      (with pos (if forwards? (+ i 1) i)
+        (tree-insert! pt pos '(""))
+        (tree-go-to pt pos 0)))))
+
+(define (proof-tree-remove-horizontal pt forwards?)
+  (let* ((prem-start (proof-tree-premise-start pt))
+         (i (proof-tree-cursor-child-index pt))
+         (n (tree-arity pt)))
+    ;; Only remove when in premises area and more than one premise
+    (when (and i (>= i prem-start) (> n (+ prem-start 1)))
+      (cond
+        (forwards?
+         (tree-remove! pt i 1)
+         (if (>= i (tree-arity pt))
+             (tree-go-to pt (- i 1) :end)
+             (tree-go-to pt i :start)))
+        ((> i prem-start)
+         (tree-remove! pt i 1)
+         (tree-go-to pt (- i 1) :end))))))
+
+(define (proof-tree-insert-vertical pt downwards?)
+  (let* ((prem-start (proof-tree-premise-start pt))
+         (i (proof-tree-cursor-child-index pt)))
+    ;; Insert sub-proof: wrap current premise in a new proof-tree
+    ;; Must explicitly set tree-label-pos to "none" to override any inherited value from parent
+    (when (and i (>= i prem-start))
+      (let* ((child-t (tree-ref pt i))
+             (content (tree->stree child-t)))
+        (if downwards?
+            ;; Insert down: add empty conclusion below, current stays as premise
+            (begin
+              (tree-set! child-t `(with "tree-mode" "proof" "tree-label-pos" "none" (tree "" ,content)))
+              (tree-go-to child-t 4 0 0))
+            ;; Insert up: wrap current as conclusion of new sub-tree with empty premise above
+            (begin
+              (tree-set! child-t `(with "tree-mode" "proof" "tree-label-pos" "none" (tree ,content "")))
+              (tree-go-to child-t 4 1 0)))))))
+
+;; Override structured-insert/remove for proof-tree
+(tm-define (structured-insert-left)
+  (:require (inside-proof-tree?))
+  (with pt (tree-innermost 'tree)
+    (when (proof-tree-tag? pt)
+      (proof-tree-insert-horizontal pt #f))))
+
+(tm-define (structured-insert-right)
+  (:require (inside-proof-tree?))
+  (with pt (tree-innermost 'tree)
+    (when (proof-tree-tag? pt)
+      (proof-tree-insert-horizontal pt #t))))
+
+(tm-define (structured-remove-left)
+  (:require (inside-proof-tree?))
+  (with pt (tree-innermost 'tree)
+    (when (proof-tree-tag? pt)
+      (proof-tree-remove-horizontal pt #f))))
+
+(tm-define (structured-remove-right)
+  (:require (inside-proof-tree?))
+  (with pt (tree-innermost 'tree)
+    (when (proof-tree-tag? pt)
+      (proof-tree-remove-horizontal pt #t))))
+
+(tm-define (structured-insert-up)
+  (:require (inside-proof-tree?))
+  (with pt (tree-innermost 'tree)
+    (proof-tree-insert-vertical pt #f)))
+
+(tm-define (structured-insert-down)
+  (:require (inside-proof-tree?))
+  (with pt (tree-innermost 'tree)
+    (proof-tree-insert-vertical pt #t)))
+
+;; Helper: check if all children of proof-tree are empty
+(define (proof-tree-all-empty? pt)
+  (let loop ((i 0))
+    (cond
+      ((>= i (tree-arity pt)) #t)
+      ((not (tree-empty? (tree-ref pt i))) #f)
+      (else (loop (+ i 1))))))
+
+;; Helper: get visual order of indices for proof-tree horizontal navigation
+;; Visual order follows the layout: left-label → premises → right-label
+;; Conclusion is excluded (accessed via up/down navigation)
+(define (proof-tree-visual-order pt)
+  (let* ((labeled? (proof-tree-labeled? pt))
+         (label-left? (and labeled? (proof-tree-label-left? pt)))
+         (prem-start (proof-tree-premise-start pt))
+         (n (tree-arity pt))
+         (premises (let loop ((i prem-start) (acc '()))
+                     (if (>= i n) (reverse acc) (loop (+ i 1) (cons i acc))))))
+    (cond
+      ((not labeled?) premises)                    ;; non-labeled: just premises
+      (label-left? (cons 0 premises))              ;; left-label: label first, then premises
+      (else (append premises (list 0))))))         ;; right-label: premises, then label
+
+;; Helper: move to adjacent field in proof-tree using visual order
+(define (proof-tree-move-to-adjacent-field pt i forwards?)
+  (let* ((order (proof-tree-visual-order pt))
+         (pos (list-find-index order (lambda (x) (== x i)))))
+    (if pos
+        (let* ((new-pos (if forwards? (+ pos 1) (- pos 1)))
+               (new-i (and (>= new-pos 0) (< new-pos (length order))
+                           (list-ref order new-pos))))
+          (cond
+            ((and new-i forwards?)
+             (tree-go-to pt new-i :start))
+            ((and new-i (not forwards?))
+             (tree-go-to pt new-i :end))
+            (else (noop))))
+        (noop))))
+
+;; Helper: check if index is a premise in the proof-tree
+(define (proof-tree-premise? pt i)
+  (let ((prem-start (proof-tree-premise-start pt)))
+    (and i (>= i prem-start))))
+
+;; Helper: count number of premises in proof-tree
+(define (proof-tree-premise-count pt)
+  (let ((prem-start (proof-tree-premise-start pt)))
+    (- (tree-arity pt) prem-start)))
+
+;; Helper: remove a premise from proof-tree and move cursor appropriately
+(define (proof-tree-remove-premise pt i forwards?)
+  (let* ((prem-start (proof-tree-premise-start pt))
+         (n (tree-arity pt)))
+    (tree-remove! pt i 1)
+    ;; Move cursor to adjacent premise
+    (cond
+      (forwards?
+       (if (>= i (tree-arity pt))
+           (tree-go-to pt (- i 1) :end)
+           (tree-go-to pt i :start)))
+      (else
+       (if (> i prem-start)
+           (tree-go-to pt (- i 1) :end)
+           (tree-go-to pt prem-start :start))))))
+
+;; Override kbd-remove for proof-tree fields
+;; When at field boundary: move to adjacent field instead of deleting structure
+;; Visual order: left-label → premises → right-label (conclusion excluded)
+;; Conclusion uses up/down navigation, so delete at its boundaries does nothing
+;; Empty premise with multiple premises: remove the premise
+;; Only delete the entire proof-tree when all fields are empty
+(tm-define (kbd-remove t forwards?)
+  (:require (and (inside-proof-tree?)
+                 (not (selection-active-any?))))
+  (with pt (tree-innermost 'tree)
+    (let* ((i (tree-down-index pt))
+           (child (and i (tree-ref pt i)))
+           (at-start (and child (tree-cursor-at? child :start)))
+           (at-end (and child (tree-cursor-at? child :end)))
+           (child-empty (and child (tree-empty? child)))
+           (is-premise (proof-tree-premise? pt i))
+           (prem-count (proof-tree-premise-count pt)))
+      (cond
+        ;; If all fields are empty and we're trying to delete, remove the whole with structure
+        ((and child-empty (proof-tree-all-empty? pt))
+         (with with-t (find-proof-tree-with pt)
+           (when with-t
+             (tree-cut with-t))))
+        ;; Empty premise with more than one premise: remove this premise
+        ((and child-empty is-premise (> prem-count 1))
+         (proof-tree-remove-premise pt i forwards?))
+        ;; Backspace at start of field: move to previous field in visual order
+        ;; (does nothing if in conclusion, as it's not in visual order)
+        ((and (not forwards?) at-start)
+         (proof-tree-move-to-adjacent-field pt i #f))
+        ;; Delete at end of field: move to next field in visual order
+        ;; (does nothing if in conclusion, as it's not in visual order)
+        ((and forwards? at-end)
+         (proof-tree-move-to-adjacent-field pt i #t))
+        ;; Otherwise, do normal text removal
+        (else (remove-text forwards?))))))
+
+;; Override remove-structure-upwards for proof-tree
+;; When inside a proof-tree, remove the entire with structure, not just the tree tag
+(tm-define (remove-structure-upwards)
+  (:require (inside-proof-tree?))
+  (with pt (tree-innermost 'tree)
+    (with with-t (find-proof-tree-with pt)
+      (if with-t
+          ;; Replace the with structure with the conclusion content
+          (let* ((conc-idx (proof-tree-conclusion-idx pt))
+                 (conclusion (tree-ref pt conc-idx)))
+            (tree-set! with-t (tree-copy conclusion))
+            (tree-go-to with-t :end))
+          ;; Fallback to default behavior
+          (former)))))
+
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; Extra editing functions
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
diff --git a/TeXmacs/progs/math/math-menu.scm b/TeXmacs/progs/math/math-menu.scm
index 6f65460d09..a3e0f4f128 100644
--- a/TeXmacs/progs/math/math-menu.scm
+++ b/TeXmacs/progs/math/math-menu.scm
@@ -1065,7 +1065,12 @@
   ("Square root" (make-sqrt))
   ("N-th root" (make-var-sqrt))
   ("Negation" (make-neg))
-  ("Tree" (make-tree))
+  (-> "Tree"
+      ("Tree" (make-tree))
+      ---
+      ("Proof tree" (make-proof-tree))
+      ("Proof tree (right label)" (make-proof-tree*))
+      ("Proof tree (left label)" (make-proof-tree**)))
   ---
   (-> "Script"
       ("Left subscript" (make-script #f #f))
@@ -1470,3 +1475,78 @@
   ;;((balloon (icon "tm_reset.xpm") "Reset to default bracket size")
   ;; (geometry-reset))
   )
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Proof tree focus menus
+;; Note: proof-tree is now a macro wrapping tree with tree-mode=proof
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(tm-define (focus-can-insert-remove? t)
+  (:require (proof-tree-tag? t))
+  #t)
+
+;; For proof-tree, we use symbolic variant names for the focus menu
+;; These don't correspond to actual tags but allow the dropdown to work
+(tm-define (focus-tag-name l)
+  (:require (== l 'proof-tree-none))
+  "Proof tree")
+
+(tm-define (focus-tag-name l)
+  (:require (== l 'proof-tree-right))
+  "Proof tree (right label)")
+
+(tm-define (focus-tag-name l)
+  (:require (== l 'proof-tree-left))
+  "Proof tree (left label)")
+
+;; Return the current variant symbol based on label position
+(define (proof-tree-current-variant t)
+  (let ((pos (proof-tree-current-label-pos t)))
+    (cond ((== pos "right") 'proof-tree-right)
+          ((== pos "left") 'proof-tree-left)
+          (else 'proof-tree-none))))
+
+;; Override focus-tag-name for tree when in proof mode
+(tm-define (focus-tag-name l)
+  (:require (and (== l 'tree) (tm-equal? (get-env-tree "tree-mode") "proof")))
+  (let ((pos (get-env-tree "tree-label-pos")))
+    (cond ((tm-equal? pos "right") "Proof tree (right label)")
+          ((tm-equal? pos "left") "Proof tree (left label)")
+          (else "Proof tree"))))
+
+;; Return 3 variants so dropdown appears
+(tm-define (focus-variants-of t)
+  (:require (proof-tree-tag? t))
+  '(proof-tree-none proof-tree-right proof-tree-left))
+
+(tm-menu (focus-variant-menu t)
+  (:require (proof-tree-tag? t))
+  (let ((current (proof-tree-current-variant t)))
+    ((check (eval (focus-tag-name 'proof-tree-none)) "v"
+            (== current 'proof-tree-none))
+     (proof-tree-set-label-pos t "none"))
+    ((check (eval (focus-tag-name 'proof-tree-right)) "v"
+            (== current 'proof-tree-right))
+     (proof-tree-set-label-pos t "right"))
+    ((check (eval (focus-tag-name 'proof-tree-left)) "v"
+            (== current 'proof-tree-left))
+     (proof-tree-set-label-pos t "left"))))
+
+(tm-menu (focus-insert-menu t)
+  (:require (proof-tree-tag? t))
+  ("Insert premise before" (structured-insert-left))
+  ("Insert premise after" (structured-insert-right))
+  ---
+  ("Insert sub-proof above" (structured-insert-up))
+  ("Remove premise" (structured-remove-right)))
+
+(tm-menu (focus-insert-icons t)
+  (:require (proof-tree-tag? t))
+  ((balloon (icon "tm_insert_left.xpm") "Insert premise before")
+   (structured-insert-left))
+  ((balloon (icon "tm_insert_right.xpm") "Insert premise after")
+   (structured-insert-right))
+  ((balloon (icon "tm_insert_up.xpm") "Insert sub-proof above")
+   (structured-insert-up))
+  ((balloon (icon "tm_delete_right.xpm") "Remove premise")
+   (structured-remove-right)))
diff --git a/TeXmacs/progs/math/math-sem-edit.scm b/TeXmacs/progs/math/math-sem-edit.scm
index 8b6f7c58a4..9acc04ea96 100644
--- a/TeXmacs/progs/math/math-sem-edit.scm
+++ b/TeXmacs/progs/math/math-sem-edit.scm
@@ -434,6 +434,9 @@
 (wrap-inserter make-wide-under)
 (wrap-inserter make-neg)
 (wrap-inserter make-tree)
+(wrap-inserter make-proof-tree)
+(wrap-inserter make-proof-tree*)
+(wrap-inserter make-proof-tree**)
 (wrap-inserter make-long-arrow)
 (wrap-inserter make-long-arrow*)
 
diff --git a/TeXmacs/progs/utils/library/cpp-wrap.scm b/TeXmacs/progs/utils/library/cpp-wrap.scm
index 41082e0bc6..f2643b86e7 100644
--- a/TeXmacs/progs/utils/library/cpp-wrap.scm
+++ b/TeXmacs/progs/utils/library/cpp-wrap.scm
@@ -109,6 +109,15 @@
 (tm-define (make-neg) (cpp-make-neg))
 (tm-define (make-tree) (cpp-make-tree))
 
+(tm-define (make-proof-tree)
+  (insert-go-to '(with "tree-mode" "proof" "tree-label-pos" "none" (tree "" "")) '(4 0 0)))
+
+(tm-define (make-proof-tree*)
+  (insert-go-to '(with "tree-mode" "proof" "tree-label-pos" "right" (tree "" "" "")) '(4 0 0)))
+
+(tm-define (make-proof-tree**)
+  (insert-go-to '(with "tree-mode" "proof" "tree-label-pos" "left" (tree "" "" "")) '(4 0 0)))
+
 (tm-define (clipboard-copy cb) (cpp-clipboard-copy cb))
 (tm-define (clipboard-cut cb) (cpp-clipboard-cut cb))
 (tm-define (clipboard-paste cb) (cpp-clipboard-paste cb))
diff --git a/moebius/moebius/drd/drd_std.cpp b/moebius/moebius/drd/drd_std.cpp
index 3d6a740666..eca47fda69 100644
--- a/moebius/moebius/drd/drd_std.cpp
+++ b/moebius/moebius/drd/drd_std.cpp
@@ -281,7 +281,7 @@ init_std_drd () {
             ->name ("wide under")
             ->name (1, "accent"));
   init (NEG, "neg", fixed (1)->accessible (0)->name ("negation"));
-  init (TREE, "tree", repeat (2, 1)->accessible (0));
+  init (TREE, "tree", repeat (2, 1)->accessible (0)->name ("tree"));
   init (SYNTAX, "syntax",
         fixed (1, 1, BIFORM)
             ->accessible (0)
diff --git a/moebius/moebius/vars.cpp b/moebius/moebius/vars.cpp
index 223f0c8b27..bbcdd7a74e 100644
--- a/moebius/moebius/vars.cpp
+++ b/moebius/moebius/vars.cpp
@@ -93,6 +93,9 @@ string MATH_TOP_SWELL_END ("math-top-swell-end");
 string MATH_BOT_SWELL_START ("math-bot-swell-start");
 string MATH_BOT_SWELL_END ("math-bot-swell-end");
 
+string TREE_MODE ("tree-mode");
+string TREE_LABEL_POS ("tree-label-pos");
+
 string PROG_LANGUAGE ("prog-language");
 string PROG_SCRIPTS ("prog-scripts");
 string PROG_FONT ("prog-font");
diff --git a/moebius/moebius/vars.hpp b/moebius/moebius/vars.hpp
index 4c1e62a559..ce0da1636d 100644
--- a/moebius/moebius/vars.hpp
+++ b/moebius/moebius/vars.hpp
@@ -87,6 +87,9 @@ extern string MATH_TOP_SWELL_END;
 extern string MATH_BOT_SWELL_START;
 extern string MATH_BOT_SWELL_END;
 
+extern string TREE_MODE;
+extern string TREE_LABEL_POS;
+
 extern string PROG_LANGUAGE;
 extern string PROG_SCRIPTS;
 extern string PROG_FONT;
diff --git a/src/Scheme/Glue/glue_editor.lua b/src/Scheme/Glue/glue_editor.lua
index 143d8b1c86..1afc80ed7f 100644
--- a/src/Scheme/Glue/glue_editor.lua
+++ b/src/Scheme/Glue/glue_editor.lua
@@ -852,7 +852,7 @@ function main()
                 cpp_name = "make_tree",
                 ret_type = "void"
             },
-            
+
             -- modify tables
             {
                 scm_name = "make-subtable",
diff --git a/src/Typeset/Boxes/Composite/math_boxes.cpp b/src/Typeset/Boxes/Composite/math_boxes.cpp
index c536165cb9..1cd0729e7e 100644
--- a/src/Typeset/Boxes/Composite/math_boxes.cpp
+++ b/src/Typeset/Boxes/Composite/math_boxes.cpp
@@ -754,6 +754,233 @@ tree_box (path ip, array<box> bs, font fn, pencil pen) {
   return tm_new<tree_box_rep> (ip, bs, fn, pen);
 }
 
+/******************************************************************************
+ * Proof tree boxes (natural deduction trees)
+ ******************************************************************************/
+
+struct proof_tree_box_rep : public composite_box_rep {
+  font   fn;
+  pencil pen;
+  SI     border;
+  bool   has_label;
+  bool   label_left;
+  int    n_children;  // Store original child count before adding decorations
+  SI     line_center; // X-coordinate of line center (for alignment with parent)
+  proof_tree_box_rep (path ip, array<box> bs, font fn, pencil pen,
+                      bool has_label, bool label_left);
+  operator tree () { return "proof-tree box"; }
+  box adjust_kerning (int mode, double factor);
+  box expand_glyphs (int mode, double factor);
+  int find_child (SI x, SI y, SI delta, bool force);
+  SI  get_leaf_offset (string search);
+};
+
+proof_tree_box_rep::proof_tree_box_rep (path ip, array<box> bs, font fn2,
+                                        pencil pen2, bool has_label2,
+                                        bool label_left2)
+    : composite_box_rep (ip), fn (fn2), pen (pen2), has_label (has_label2),
+      label_left (label_left2), n_children (N (bs)) {
+  // For labeled: bs[0] is label, bs[1] is conclusion, bs[2..n-1] are premises
+  // For unlabeled: bs[0] is conclusion, bs[1..n-1] are premises
+  // n_children stores original count before adding decoration line box
+  //
+  // IMPORTANT: Insert boxes in ORIGINAL ORDER (0, 1, 2, ..., n-1) first,
+  // then add line box LAST. This ensures internal bs array indices match
+  // original indices for find_child to work correctly.
+  //
+  // KEY ALIGNMENT PRINCIPLE: The box is centered on its inference line center.
+  // This means x=0 corresponds to the line center, so when this box is used
+  // as a premise in a parent proof-tree, the parent will align by line centers.
+  SI sep     = fn->sep;
+  SI min_hsep= fn->wfn; // minimum horizontal space between premises
+  SI hsep    = max (2 * fn->spc->def, min_hsep);
+  SI vsep    = 2 * fn->spc->def;
+  SI line_w  = fn->wline;
+  SI label_sp= fn->spc->def; // space between line and label
+
+  int i, n= N (bs);
+  int conc_idx  = has_label ? 1 : 0;
+  int prem_start= has_label ? 2 : 1;
+
+  // Calculate premises layout info
+  // For proper spacing with alignment, we need left/right extents from
+  // alignment point This prevents overlap when child proof-trees have labels
+  // extending beyond their lines
+  SI max_y2= MIN_SI;
+  SI min_y1= MAX_SI;
+
+  // Calculate align offsets (line center or geometric center) for all premises
+  array<SI> align_offsets (n);
+  array<SI> left_extents (n);  // distance from box x1 to alignment point
+  array<SI> right_extents (n); // distance from alignment point to box x2
+  for (i= prem_start; i < n; i++) {
+    SI offset= bs[i]->get_leaf_offset ("line_center");
+    if (offset == bs[i]->w ()) {
+      // Default return - not a proof-tree, use geometric center
+      offset= (bs[i]->x1 + bs[i]->x2) >> 1;
+    }
+    align_offsets[i]= offset;
+    left_extents[i] = offset;
+    right_extents[i]= bs[i]->w () - offset;
+    max_y2          = max (max_y2, bs[i]->y2);
+    min_y1          = min (min_y1, bs[i]->y1);
+  }
+
+  // Calculate total premises width based on proper spacing:
+  // Total = left_ext[first] + sum(right_ext[i] + hsep + left_ext[i+1]) +
+  // right_ext[last]
+  SI prem_w= 0;
+  for (i= prem_start; i < n; i++) {
+    if (i == prem_start) {
+      prem_w+= left_extents[i]; // First premise: count left extent
+    }
+    prem_w+= right_extents[i]; // Count right extent
+    if (i < n - 1) {
+      prem_w+= hsep;                // Add spacing between premises
+      prem_w+= left_extents[i + 1]; // Next premise's left extent
+    }
+  }
+
+  // Calculate conclusion dimensions
+  SI conc_w= bs[conc_idx]->w ();
+
+  // Calculate label width if present
+  SI label_w= has_label ? bs[0]->w () : 0;
+
+  // Calculate inference line width (covers premises and conclusion)
+  SI line_margin = fn->spc->def;
+  SI line_w_total= max (prem_w, conc_w) + 2 * line_margin;
+
+  // Line extends from -line_w_total/2 to +line_w_total/2 (centered on 0)
+  SI line_half= line_w_total >> 1;
+  SI line_x1  = -line_half;
+  SI line_x2  = line_half;
+  SI line_y   = max (bs[conc_idx]->y2, fn->y2) + (vsep >> 1);
+
+  // Calculate premise baseline
+  SI prem_baseline= max (bs[conc_idx]->y2, fn->y2) + sep + vsep - min_y1;
+
+  // Store positions for each child box
+  array<SI> pos_x (n);
+  array<SI> pos_y (n);
+
+  // Position premises centered on line, aligned by their line centers
+  // Use pre-calculated align_offsets and extents for proper spacing
+  if (n > prem_start) {
+    SI prem_half= prem_w >> 1;
+    // align_x tracks where the current premise's alignment point should be
+    SI align_x= -prem_half + left_extents[prem_start];
+    for (i= prem_start; i < n; i++) {
+      // Position box so its alignment point is at align_x
+      pos_x[i]= align_x - align_offsets[i];
+      pos_y[i]= prem_baseline;
+      // Advance to next alignment point: current right extent + hsep + next
+      // left extent
+      if (i < n - 1) {
+        align_x+= right_extents[i] + hsep + left_extents[i + 1];
+      }
+    }
+  }
+
+  // Position conclusion centered on line (0 point)
+  SI conc_center = (bs[conc_idx]->x1 + bs[conc_idx]->x2) >> 1;
+  pos_x[conc_idx]= -conc_center;
+  pos_y[conc_idx]= 0;
+
+  // Position label if present
+  if (has_label) {
+    pos_y[0]= line_y - ((bs[0]->y1 + bs[0]->y2) >> 1);
+    if (label_left) {
+      // Label is to the left of line: ends at line_x1 - label_sp
+      pos_x[0]= line_x1 - label_sp - bs[0]->x2;
+    }
+    else {
+      // Label is to the right of line: starts at line_x2 + label_sp
+      pos_x[0]= line_x2 + label_sp - bs[0]->x1;
+    }
+  }
+
+  // Now insert boxes in ORIGINAL ORDER (0, 1, 2, ..., n-1)
+  for (i= 0; i < n; i++) {
+    insert (bs[i], pos_x[i], pos_y[i]);
+  }
+
+  // Insert line box LAST (so it doesn't interfere with child indices)
+  pencil tpen= pen->set_width (line_w);
+  insert (line_box (decorate_middle (ip), line_x1, 0, line_x2, 0, tpen), 0,
+          line_y);
+
+  position ();
+  border= line_y;
+
+  // Store line center position before left_justify
+  // Since we centered on x=0, line_center is currently 0
+  // After left_justify(), line_center becomes -old_x1
+  SI old_x1  = x1;
+  line_center= 0;
+  left_justify ();
+  line_center= -old_x1; // Now relative to x1=0
+
+  finalize ();
+}
+
+box
+proof_tree_box_rep::adjust_kerning (int mode, double factor) {
+  (void) mode;
+  // Use n_children to exclude the decoration line box
+  array<box> adj (n_children);
+  for (int i= 0; i < n_children; i++)
+    adj[i]= bs[i]->adjust_kerning (0, factor);
+  return proof_tree_box (ip, adj, fn, pen, has_label, label_left);
+}
+
+box
+proof_tree_box_rep::expand_glyphs (int mode, double factor) {
+  (void) mode;
+  // Use n_children to exclude the decoration line box
+  array<box> adj (n_children);
+  for (int i= 0; i < n_children; i++)
+    adj[i]= bs[i]->expand_glyphs (0, factor);
+  return proof_tree_box (ip, adj, fn, pen, has_label, label_left);
+}
+
+int
+proof_tree_box_rep::find_child (SI x, SI y, SI delta, bool force) {
+  if (outside (x, delta, x1, x2) && (is_accessible (ip) || force)) return -1;
+  int conc_idx= has_label ? 1 : 0;
+  int i       = conc_idx;
+  // Conclusion is below the border, premises above
+  if (y > border) {
+    int prem_start= has_label ? 2 : 1;
+    int j, d= MAX_SI;
+    // Use n_children (not N(bs)) to exclude decoration line box
+    for (j= prem_start; j < n_children; j++)
+      if (distance (j, x, y, delta) < d)
+        if (bs[j]->accessible () || force) {
+          d= distance (j, x, y, delta);
+          i= j;
+        }
+  }
+  // Check if clicking on label
+  if (has_label && distance (0, x, y, delta) < distance (i, x, y, delta))
+    if (bs[0]->accessible () || force) i= 0;
+  if (bs[i]->decoration () && (!force)) return -1;
+  return i;
+}
+
+SI
+proof_tree_box_rep::get_leaf_offset (string search) {
+  // Return the line center as alignment point for parent proof-trees
+  if (search == "line_center") return line_center;
+  return composite_box_rep::get_leaf_offset (search);
+}
+
+box
+proof_tree_box (path ip, array<box> bs, font fn, pencil pen, bool has_label,
+                bool label_left) {
+  return tm_new<proof_tree_box_rep> (ip, bs, fn, pen, has_label, label_left);
+}
+
 box
 wide_box (path ip, box ref, string s, font fn, pencil pen, bool wf, bool af) {
   return tm_new<wide_box_rep> (ip, ref, s, fn, pen, wf, af);
diff --git a/src/Typeset/Boxes/construct.hpp b/src/Typeset/Boxes/construct.hpp
index 28b665394d..92cb139f51 100644
--- a/src/Typeset/Boxes/construct.hpp
+++ b/src/Typeset/Boxes/construct.hpp
@@ -151,6 +151,8 @@ box frac_box (path ip, box b1, box b2, font fn, font sfn, pencil pen,
 box sqrt_box (path ip, box b1, box b2, box sqrtb, font fn, pencil pen);
 box neg_box (path ip, box b, font fn, pencil pen);
 box tree_box (path ip, array<box> bs, font fn, pencil pen);
+box proof_tree_box (path ip, array<box> bs, font fn, pencil pen,
+                    bool has_label= false, bool label_left= false);
 box wide_box (path ip, box ref, string s, font fn, pencil p, bool wf, bool af);
 box repeat_box (path ip, box ref, box repeat, SI xoff= 0, bool under= false);
 box limit_box (path ip, box ref, box lo, box hi, font fn, bool glued);
diff --git a/src/Typeset/Concat/concat_math.cpp b/src/Typeset/Concat/concat_math.cpp
index 48a24619c1..c89da5b0b4 100644
--- a/src/Typeset/Concat/concat_math.cpp
+++ b/src/Typeset/Concat/concat_math.cpp
@@ -612,11 +612,36 @@ concater_rep::typeset_tree (tree t, path ip) {
     typeset_error (t, ip);
     return;
   }
-  int        i, n= N (t);
-  array<box> bs (n);
-  for (i= 0; i < n; i++)
-    bs[i]= typeset_as_concat (env, t[i], descend (ip, i));
-  print (tree_box (ip, bs, env->fn, env->pen));
+
+  // Check tree-mode environment variable
+  string mode= as_string (env->read (TREE_MODE));
+
+  if (mode == "proof") {
+    // Proof tree mode: check for label position
+    string label_pos = as_string (env->read (TREE_LABEL_POS));
+    bool   has_label = (label_pos == "left" || label_pos == "right");
+    bool   label_left= (label_pos == "left");
+
+    int min_children= has_label ? 3 : 2;
+    if (N (t) < min_children) {
+      typeset_error (t, ip);
+      return;
+    }
+
+    int        i, n= N (t);
+    array<box> bs (n);
+    for (i= 0; i < n; i++)
+      bs[i]= typeset_as_concat (env, t[i], descend (ip, i));
+    print (proof_tree_box (ip, bs, env->fn, env->pen, has_label, label_left));
+  }
+  else {
+    // Normal tree mode (default)
+    int        i, n= N (t);
+    array<box> bs (n);
+    for (i= 0; i < n; i++)
+      bs[i]= typeset_as_concat (env, t[i], descend (ip, i));
+    print (tree_box (ip, bs, env->fn, env->pen));
+  }
 }
 
 void
diff --git a/src/Typeset/Env/env_default.cpp b/src/Typeset/Env/env_default.cpp
index 04cd67794e..b6a8730d64 100644
--- a/src/Typeset/Env/env_default.cpp
+++ b/src/Typeset/Env/env_default.cpp
@@ -110,6 +110,9 @@ initialize_default_env () {
   env (MATH_BOT_SWELL_START)= "-0.7ex";   // start padding below this level
   env (MATH_BOT_SWELL_END)  = "-2.5ex";   // maximal padding reached here
 
+  env (TREE_MODE)     = "normal"; // tree rendering mode: "normal" or "proof"
+  env (TREE_LABEL_POS)= "none"; // tree label position: "none", "left", "right"
+
   env (PROG_LANGUAGE)   = "scheme";  // the default programming language
   env (PROG_SCRIPTS)    = "none";    // the scripting language
   env (PROG_FONT)       = "roman";   // the font name in prog mode