Code Golf

#5: Post edited by

CrSb0001‭ · 2025-04-14T16:36:46Z (5 days ago)
-15 bytes

Copy Link

Raw

Markdown

~~# [Lean 4], <s>115</s> <s>109</s> 104 bytes~~
Note: had to update bytecount to take into account non-printable characters.
---
For anyone who isn't familiar with Lean, it's basically an interactive theorem prover that can also be used for regular math computation. Those who are familiar with Haskell would probably be able to recognize some of the syntax used, such as the `<$>` functor that represents the mapping of a function onto a range.
~~Also you can shove most functions on one line for whatever reason. xD~~
---
Something else to mention is that I forgot until now that I could simply omit the case where the input is 1. This is because since I am defining the function on `Nat -> Nat`, that means when I compute `g(1)`, I actually compute$$\begin{align}g(1)&=2+3*g(1-1)+4*g(1-2)+2\sum_{n=0}^{1-2}g(n)\\&=2+3*g(0)+4*g(0)+2*\sum_{n=0}^0g(n)\\&=2+0+0+0=2\end{align}$$Since on the natural numbers, Lean defines $a-b=0$ when $a\le b$.
---
```lean
~~import Mathlib~~
~~def g:Nat→Nat|0=>0|n=>2+(g (n-1))*3+(g (n-2))*4+2*((λx=>g x)<$>(List.Ico 0 (n-2))).sum~~
```
[Try it online!] (ungolfed version) Link leads to the test case `g(24) = 284925519302420`. Not using TIO as that only supports Lean 3.
---
Hexdump:
```none
~~00000000 69 6d 70 6f 72 74 20 4d 61 74 68 6c 69 62 10 64 |import Mathlib.d|~~
00000010 65 66 20 67 3a 4e 61 74 e2 86 92 4e 61 74 7c 30 |ef g:Nat...Nat|0|
~~00000020 3d 3e 30 7c 6e 3d 3e 32 2b 28 67 20 28 6e 2d 31 |=>0|n=>2+(g (n-1|~~
~~00000030 29 29 2a 33 2b 28 67 20 28 6e 2d 32 29 29 2a 34 |))*3+(g (n-2))*4|~~
~~00000040 2b 32 2a 28 28 ce bb 78 3d 3e 67 20 78 29 3c 24 |+2*((..x=>g x)<$|~~
~~00000050 3e 28 4c 69 73 74 2e 49 63 6f 20 30 20 28 6e 2d |>(List.Ico 0 (n-|~~
~~00000060 32 29 29 29 2e 73 75 6d |2))).sum|~~
```
---
Something to clarify about this: While I did not prove that this eventually terminates, or set a recursion depth using `set_option diagnostics.threshold`, neither of those things are actually needed.
This is because I can simply use `#eval!` instead of `#eval` to evaluate the function without needing to do either of those things.
[Lean 4]:https://lean-lang.org/
[Try it online!]:https://live.lean-lang.org/#codez=JYWwDg9gTgLgBAWQIYwBYBtgCMBQATAUwDM4BzALgDkVAkwmphwB84AGAXgD4Wm4BGTgEw8AdoIDUAClJwJwgLS8AlIoBUAZknTZcgcpUAWMQJUSJgbuAAHp2kXFAHgAkHCQBlgAZxgA6AJIBjCFYZeV1lL3cAVxAcHABiAgA3JHQAQjI4AX0gA

# [Lean 4], <s>115</s> <s>109</s> <s>104</s> 89 bytes
Note: had to update bytecount to take into account non-printable characters.
---
For anyone who isn't familiar with Lean, it's basically an interactive theorem prover that can also be used for regular math computation. Those who are familiar with Haskell would probably be able to recognize some of the syntax used, such as the `<$>` functor that represents the mapping of a function onto a range.
Also you can shove most functions on one line for whatever reason, and you only need to import Mathlib if you are using `List.Ico`, whereas I can just use `List.range` for the same effect. xD
---
Something else to mention is that I forgot until now that I could simply omit the case where the input is 1. This is because since I am defining the function on `Nat -> Nat`, that means when I compute `g(1)`, I actually compute$$\begin{align}g(1)&=2+3*g(1-1)+4*g(1-2)+2\sum_{n=0}^{1-2}g(n)\\&=2+3*g(0)+4*g(0)+2*\sum_{n=0}^0g(n)\\&=2+0+0+0=2\end{align}$$Since on the natural numbers, Lean defines $a-b=0$ when $a\le b$.
---
```lean
def g:Nat→Nat|0=>0|n=>2+(g (n-1))*3+(g (n-2))*4+2*((λx=>g x)<$>(List.range (n-2))).sum
```
[Try it online!] (ungolfed version) Link leads to the test case `g(24) = 284925519302420`. Not using TIO as that only supports Lean 3.
---
Hexdump:
```none
00000000 64 65 66 20 67 3a 4e 61 74 e2 86 92 4e 61 74 7c |def g:Nat...Nat||
00000010 30 3d 3e 30 7c 6e 3d 3e 32 2b 28 67 20 28 6e 2d |0=>0|n=>2+(g (n-|
00000020 31 29 29 2a 33 2b 28 67 20 28 6e 2d 32 29 29 2a |1))*3+(g (n-2))*|
00000030 34 2b 32 2a 28 28 ce bb 78 3d 3e 67 20 78 29 3c |4+2*((..x=>g x)<|
00000040 24 3e 28 4c 69 73 74 2e 72 61 6e 67 65 20 28 6e |$>(List.range (n|
00000050 2d 32 29 29 29 2e 73 75 6d |-2))).sum|
```
---
Something to clarify about this: While I did not prove that this eventually terminates, or set a recursion depth using `set_option diagnostics.threshold`, neither of those things are actually needed.
This is because I can simply use `#eval!` instead of `#eval` to evaluate the function without needing to do either of those things.
[Lean 4]:https://lean-lang.org/
[Try it online!]:https://live.lean-lang.org/#codez=JYWwDg9gTgLgBAWQIYwBYBtgCMBQATAUwDM4BzALgDkVAkwmphwB84AGAXgD4Wm4BGTgEw8AdoIDUAClJwJwgLS8AlIoBUAZknTZcgcpUAWMQJUSJgbuAAHp2kXFAHgAkHCQBlgAZxgA6AJIBjCFYZeV1lL3cAVxAcHABiAgA3JHQAQjI4AX0gA

#4: Post edited by

CrSb0001‭ · 2025-04-14T15:08:39Z (5 days ago)
-5 bytes

Copy Link

Raw

Markdown

~~# [Lean 4], <s>115</s> 109 bytes~~
Note: had to update bytecount to take into account non-printable characters.
---
For anyone who isn't familiar with Lean, it's basically an interactive theorem prover that can also be used for regular math computation. Those who are familiar with Haskell would probably be able to recognize some of the syntax used, such as the `<$>` functor that represents the mapping of a function onto a range.
Also you can shove most functions on one line for whatever reason. xD
```lean
import Mathlib
~~def g:Nat→Nat|0=>0|1=>2|n=>2+(g (n-1))*3+(g (n-2))*4+2*((λx=>g x)<$>(List.Ico 0 (n-2))).sum~~
```
[Try it online!] (ungolfed version) Link leads to the test case `g(24) = 284925519302420`. Not using TIO as that only supports Lean 3.
---
Hexdump:
```none
00000000 69 6d 70 6f 72 74 20 4d 61 74 68 6c 69 62 10 64 |import Mathlib.d|
00000010 65 66 20 67 3a 4e 61 74 e2 86 92 4e 61 74 7c 30 |ef g:Nat...Nat|0|
~~00000020 3d 3e 30 7c 31 3d 3e 32 7c 6e 3d 3e 32 2b 28 67 |=>0|1=>2|n=>2+(g|~~
~~00000030 20 28 6e 2d 31 29 29 2a 33 2b 28 67 20 28 6e 2d | (n-1))*3+(g (n-|~~
~~00000040 32 29 29 2a 34 2b 32 2a 28 28 ce bb 78 3d 3e 67 |2))*4+2*((..x=>g|~~
~~00000050 20 78 29 3c 24 3e 28 4c 69 73 74 2e 49 63 6f 20 | x)<$>(List.Ico |~~
~~00000060 30 20 28 6e 2d 32 29 29 29 2e 73 75 6d |0 (n-2))).sum|~~
```
---
Something to clarify about this: While I did not prove that this eventually terminates, or set a recursion depth using `set_option diagnostics.threshold`, neither of those things are actually needed.
This is because I can simply use `#eval!` instead of `#eval` to evaluate the function without needing to do either of those things.
[Lean 4]:https://lean-lang.org/
[Try it online!]:https://live.lean-lang.org/#codez=JYWwDg9gTgLgBAWQIYwBYBtgCMBQATAUwDM4BzALgDkVAkwmphwB84AGAXgD4Wm4BGTgEw8AdoIDUAClJwJwgLS8AlIoBUAZknTZcgcpUAWMQJUSJgbuAAHp2kXFAHgAkHCQBlgAZxgA6AJIBjCFYZeV1lL3cAVxAcHABiAgA3JHQAQjI4AX0gA

# [Lean 4], <s>115</s> <s>109</s> 104 bytes
Note: had to update bytecount to take into account non-printable characters.
---
For anyone who isn't familiar with Lean, it's basically an interactive theorem prover that can also be used for regular math computation. Those who are familiar with Haskell would probably be able to recognize some of the syntax used, such as the `<$>` functor that represents the mapping of a function onto a range.
Also you can shove most functions on one line for whatever reason. xD
---
Something else to mention is that I forgot until now that I could simply omit the case where the input is 1. This is because since I am defining the function on `Nat -> Nat`, that means when I compute `g(1)`, I actually compute$$\begin{align}g(1)&=2+3*g(1-1)+4*g(1-2)+2\sum_{n=0}^{1-2}g(n)\\&=2+3*g(0)+4*g(0)+2*\sum_{n=0}^0g(n)\\&=2+0+0+0=2\end{align}$$Since on the natural numbers, Lean defines $a-b=0$ when $a\le b$.
---
```lean
import Mathlib
def g:Nat→Nat|0=>0|n=>2+(g (n-1))*3+(g (n-2))*4+2*((λx=>g x)<$>(List.Ico 0 (n-2))).sum
```
[Try it online!] (ungolfed version) Link leads to the test case `g(24) = 284925519302420`. Not using TIO as that only supports Lean 3.
---
Hexdump:
```none
00000000 69 6d 70 6f 72 74 20 4d 61 74 68 6c 69 62 10 64 |import Mathlib.d|
00000010 65 66 20 67 3a 4e 61 74 e2 86 92 4e 61 74 7c 30 |ef g:Nat...Nat|0|
00000020 3d 3e 30 7c 6e 3d 3e 32 2b 28 67 20 28 6e 2d 31 |=>0|n=>2+(g (n-1|
00000030 29 29 2a 33 2b 28 67 20 28 6e 2d 32 29 29 2a 34 |))*3+(g (n-2))*4|
00000040 2b 32 2a 28 28 ce bb 78 3d 3e 67 20 78 29 3c 24 |+2*((..x=>g x)<$|
00000050 3e 28 4c 69 73 74 2e 49 63 6f 20 30 20 28 6e 2d |>(List.Ico 0 (n-|
00000060 32 29 29 29 2e 73 75 6d |2))).sum|
```
---
Something to clarify about this: While I did not prove that this eventually terminates, or set a recursion depth using `set_option diagnostics.threshold`, neither of those things are actually needed.
This is because I can simply use `#eval!` instead of `#eval` to evaluate the function without needing to do either of those things.
[Lean 4]:https://lean-lang.org/
[Try it online!]:https://live.lean-lang.org/#codez=JYWwDg9gTgLgBAWQIYwBYBtgCMBQATAUwDM4BzALgDkVAkwmphwB84AGAXgD4Wm4BGTgEw8AdoIDUAClJwJwgLS8AlIoBUAZknTZcgcpUAWMQJUSJgbuAAHp2kXFAHgAkHCQBlgAZxgA6AJIBjCFYZeV1lL3cAVxAcHABiAgA3JHQAQjI4AX0gA

#3: Post edited by

CrSb0001‭ · 2025-04-11T15:20:34Z (8 days ago)
Updated bytecount to take into account non-printable characters.

Copy Link

Raw

Markdown

~~# [Lean 4], <s>112</s> 106 bytes~~
For anyone who isn't familiar with Lean, it's basically an interactive theorem prover that can also be used for regular math computation. Those who are familiar with Haskell would probably be able to recognize some of the syntax used, such as the `<$>` functor that represents the mapping of a function onto a range.
~~Also you can shove most functions on one line for whatever reason. xD[]()~~
```lean
import Mathlib
def g:Nat→Nat|0=>0|1=>2|n=>2+(g (n-1))*3+(g (n-2))*4+2*((λx=>g x)<$>(List.Ico 0 (n-2))).sum
```
~~[Try it online!] (112 byte version) Link leads to the test case `g(24) = 284925519302420`. Not using TIO as that only supports Lean 3.~~
---
Something to clarify about this: While I did not prove that this eventually terminates, or set a recursion depth using `set_option diagnostics.threshold`, neither of those things are actually needed.
This is because I can simply use `#eval!` instead of `#eval` to evaluate the function without needing to do either of those things.
[Lean 4]:https://lean-lang.org/
[Try it online!]:https://live.lean-lang.org/#codez=JYWwDg9gTgLgBAWQIYwBYBtgCMBQATAUwDM4BzALgDkVAkwmphwB84AGAXgD4Wm4BGTgEw8AdoIDUAClJwJwgLS8AlIoBUAZknTZcgcpUAWMQJUSJgbuAAHp2kXFAHgAkHCQBlgAZxgA6AJIBjCFYZeV1lL3cAVxAcHABiAgA3JHQAQjI4AX0gA

# [Lean 4], <s>115</s> 109 bytes
Note: had to update bytecount to take into account non-printable characters.
---
For anyone who isn't familiar with Lean, it's basically an interactive theorem prover that can also be used for regular math computation. Those who are familiar with Haskell would probably be able to recognize some of the syntax used, such as the `<$>` functor that represents the mapping of a function onto a range.
Also you can shove most functions on one line for whatever reason. xD
```lean
import Mathlib
def g:Nat→Nat|0=>0|1=>2|n=>2+(g (n-1))*3+(g (n-2))*4+2*((λx=>g x)<$>(List.Ico 0 (n-2))).sum
```
[Try it online!] (ungolfed version) Link leads to the test case `g(24) = 284925519302420`. Not using TIO as that only supports Lean 3.
---
Hexdump:
```none
00000000 69 6d 70 6f 72 74 20 4d 61 74 68 6c 69 62 10 64 |import Mathlib.d|
00000010 65 66 20 67 3a 4e 61 74 e2 86 92 4e 61 74 7c 30 |ef g:Nat...Nat|0|
00000020 3d 3e 30 7c 31 3d 3e 32 7c 6e 3d 3e 32 2b 28 67 |=>0|1=>2|n=>2+(g|
00000030 20 28 6e 2d 31 29 29 2a 33 2b 28 67 20 28 6e 2d | (n-1))*3+(g (n-|
00000040 32 29 29 2a 34 2b 32 2a 28 28 ce bb 78 3d 3e 67 |2))*4+2*((..x=>g|
00000050 20 78 29 3c 24 3e 28 4c 69 73 74 2e 49 63 6f 20 | x)<$>(List.Ico |
00000060 30 20 28 6e 2d 32 29 29 29 2e 73 75 6d |0 (n-2))).sum|
```
---
Something to clarify about this: While I did not prove that this eventually terminates, or set a recursion depth using `set_option diagnostics.threshold`, neither of those things are actually needed.
This is because I can simply use `#eval!` instead of `#eval` to evaluate the function without needing to do either of those things.
[Lean 4]:https://lean-lang.org/
[Try it online!]:https://live.lean-lang.org/#codez=JYWwDg9gTgLgBAWQIYwBYBtgCMBQATAUwDM4BzALgDkVAkwmphwB84AGAXgD4Wm4BGTgEw8AdoIDUAClJwJwgLS8AlIoBUAZknTZcgcpUAWMQJUSJgbuAAHp2kXFAHgAkHCQBlgAZxgA6AJIBjCFYZeV1lL3cAVxAcHABiAgA3JHQAQjI4AX0gA

#2: Post edited by

CrSb0001‭ · 2025-04-10T16:45:24Z (9 days ago)
-6 bytes

Copy Link

Raw

Markdown

~~# [Lean 4], 112 bytes~~
For anyone who isn't familiar with Lean, it's basically an interactive theorem prover that can also be used for regular math computation. Those who are familiar with Haskell would probably be able to recognize some of the syntax used, such as the `<$>` functor that represents the mapping of a function onto a range.
```lean
import Mathlib
~~def g:Nat→Nat~~
~~| 0=>0~~
~~| 1=>2~~
~~| n=>2+(g (n-1))*3+(g (n-2))*4+2*((λx=>g x)<$>(List.Ico 0 (n-2))).sum~~
```
~~[Try it online!] Link leads to the test case `g(24) = 284925519302420`. Not using TIO as that only supports Lean 3.~~
---
Something to clarify about this: While I did not prove that this eventually terminates, or set a recursion depth using `set_option diagnostics.threshold`, neither of those things are actually needed.
This is because I can simply use `#eval!` instead of `#eval` to evaluate the function without needing to do either of those things.
[Lean 4]:https://lean-lang.org/
[Try it online!]:https://live.lean-lang.org/#codez=JYWwDg9gTgLgBAWQIYwBYBtgCMBQATAUwDM4BzALgDkVAkwmphwB84AGAXgD4Wm4BGTgEw8AdoIDUAClJwJwgLS8AlIoBUAZknTZcgcpUAWMQJUSJgbuAAHp2kXFAHgAkHCQBlgAZxgA6AJIBjCFYZeV1lL3cAVxAcHABiAgA3JHQAQjI4AX0gA

# [Lean 4], <s>112</s> 106 bytes
For anyone who isn't familiar with Lean, it's basically an interactive theorem prover that can also be used for regular math computation. Those who are familiar with Haskell would probably be able to recognize some of the syntax used, such as the `<$>` functor that represents the mapping of a function onto a range.
Also you can shove most functions on one line for whatever reason. xD[]()
```lean
import Mathlib
def g:Nat→Nat|0=>0|1=>2|n=>2+(g (n-1))*3+(g (n-2))*4+2*((λx=>g x)<$>(List.Ico 0 (n-2))).sum
```
[Try it online!] (112 byte version) Link leads to the test case `g(24) = 284925519302420`. Not using TIO as that only supports Lean 3.
---
Something to clarify about this: While I did not prove that this eventually terminates, or set a recursion depth using `set_option diagnostics.threshold`, neither of those things are actually needed.
This is because I can simply use `#eval!` instead of `#eval` to evaluate the function without needing to do either of those things.
[Lean 4]:https://lean-lang.org/
[Try it online!]:https://live.lean-lang.org/#codez=JYWwDg9gTgLgBAWQIYwBYBtgCMBQATAUwDM4BzALgDkVAkwmphwB84AGAXgD4Wm4BGTgEw8AdoIDUAClJwJwgLS8AlIoBUAZknTZcgcpUAWMQJUSJgbuAAHp2kXFAHgAkHCQBlgAZxgA6AJIBjCFYZeV1lL3cAVxAcHABiAgA3JHQAQjI4AX0gA

#1: Initial revision by

CrSb0001‭ · 2025-04-10T14:20:34Z (9 days ago)

Copy Link

Raw

Markdown

# [Lean 4], 112 bytes

For anyone who isn't familiar with Lean, it's basically an interactive theorem prover that can also be used for regular math computation. Those who are familiar with Haskell would probably be able to recognize some of the syntax used, such as the `<$>` functor that represents the mapping of a function onto a range.

```lean
import Mathlib
def g:Nat→Nat
| 0=>0
| 1=>2
| n=>2+(g (n-1))*3+(g (n-2))*4+2*((λx=>g x)<$>(List.Ico 0 (n-2))).sum
```
[Try it online!] Link leads to the test case `g(24) = 284925519302420`. Not using TIO as that only supports Lean 3.

---

Something to clarify about this: While I did not prove that this eventually terminates, or set a recursion depth using `set_option diagnostics.threshold`, neither of those things are actually needed.

This is because I can simply use `#eval!` instead of `#eval` to evaluate the function without needing to do either of those things.

[Lean 4]:https://lean-lang.org/
[Try it online!]:https://live.lean-lang.org/#codez=JYWwDg9gTgLgBAWQIYwBYBtgCMBQATAUwDM4BzALgDkVAkwmphwB84AGAXgD4Wm4BGTgEw8AdoIDUAClJwJwgLS8AlIoBUAZknTZcgcpUAWMQJUSJgbuAAHp2kXFAHgAkHCQBlgAZxgA6AJIBjCFYZeV1lL3cAVxAcHABiAgA3JHQAQjI4AX0gA

Communities

Post History